CSR: Small: SMT-Aware Real Constraint Solving

计算机通常用于执行数值计算，但它们也可以进行符号计算。符号计算是必需的，例如，当目标不是数值模拟系统，而是设计或彻底验证系统时。塔斯基关于实数理论的可决性的开创性成果表明，非线性约束可以用符号求解。然而，目前可用的求解器并不是为实践中所需的特性——可伸缩性、表达性和可扩展性——而设计的。这个项目开发了一个符号推理引擎，它同时是高效和富有表现力的，它包括了基于实数理论的非线性推理。该方法将实闭场理论与现有的可满足模理论（SMT）求解方法相结合。SMT求解器是通用的、广泛使用的符号求解器，但它们目前缺乏对非线性算法推理的支持。受混合动力系统验证应用的启发，该项目探索了实数理论中的推理方法，该方法可以用完整性换取效率，并可以集成到现有的SMT求解器中。SMT解算器中非线性推理的可用性将使常规构建使用符号推理的应用程序变得更容易，特别是对于不熟悉符号方法的用户。它将使几个新的应用跨越科学和工程的广泛范围，如机器人，安全关键控制系统，嵌入式系统和系统生物学。

Computers are commonly used to perform numerical computation, but they can also compute symbolically. Symbolic computation is required, for example, when instead of numerically simulating a system, the goal is to design or exhaustively verify a system. Tarski's seminal result on decidability of the theory of reals showed that nonlinear constraints can be symbolically solved. However, the currently available solvers are not designed for the features--scalability, expressiveness, and extensibility--that are required in practice.This project develops a symbolic reasoning engine that is simultaneously efficient and expressive, and that includes nonlinear reasoning over the theory of reals. The approach is based on integrating the theory of real closed fields with existing theories supported by Satisfiability Modulo Theory (SMT) solvers. SMT solvers are general-purpose, widely used, symbolic solvers, but they currently lack support for reasoning over nonlinear arithmetic. Motivated by the application to verification of hybrid dynamical systems, this project explores an approach for reasoning in the theory of reals that can trade completeness for efficiency and can be integrated within existing SMT solvers.The availability of nonlinear reasoning in SMT solvers will make it easier, especially for users not skilled in symbolic methods, to routinely build applications that use symbolic reasoning. It will enable several new applications spanning a wide spectrum of science and engineering, such as robotics, safety-critical control systems, embedded systems, and systems biology.