CSR: Small: SMT-Aware Real Constraint Solving

Sri International, Menlo Park CA

Investigators

Abstract

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.