Formal Verification via Boolean and Theory Reasoning (SMT)

State of the art techniques used in Formal Verification ultimately rely on the expression of properties (of the system to verify) in terms of languages that can be easily understood and processed by automatic tools.

One of the most used languages nowadays is Boolean logic at the propositional level; its associated decision problem, SAT, has been extensively studied in the latest decade. The reason for the success of SAT is twofold (i) for the simplicity and flexibility of propositional logic and (ii) for the availability of extremely efficient and robust tools for deciding SAT (SAT-Solvers).

Satisfiability Modulo Theories (SMT for short) is a novel paradigm that supports encoding of formal properties at a higher level of expressiveness than Booleans. Beside propositional logic, the language (that comes with different flavors) allows for the expression of other useful theories, such as linear arithmetic or bit-vectors. The language of SMT can be therefore used to replace simple Boolean logic or to express properties that cannot be encoded into SAT.

As for SAT, the need of automatic tools in formal verification led to the development of SMT-Solvers. SMT-Solvers are based on the same engine of SAT-Solvers, and they integrate theory reasoning and Boolean reasoning in an elegant and efficient framework.

This project focuses on the development of efficient SMT-Solvers, and on the application of SMT instead of SAT in the domain of formal verification. Our current results include papers [1], [2] and the tool - OpenSMT solver, the basic SMT-solving framework we use for all experiments.

References