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) the simplicity and flexibility of propositional logic and (ii) 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, arrays and 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 effective framework.

A first goal of the project consists in the development of new efficient decision procedures for SMT, and in the application of SMT instead of SAT in the domain of Formal Verification.

From the point of view of Formal Verification, the problem of determining if a system respects a certain property can be effectively translated into verifying the satisfiability of a logic formula encoding both the system and the property.

In case the formula under examination does not admit a model, SAT and SMT-Solvers can be easily instructed to produce a certificate in the form of a propositional resolution proof of unsatisfiability, by keeping track of the steps performed while looking for such a model.

A remarkable application of resolution proofs within the field of Model Checking is related to the generation of mathematical objects called interpolants. We can think of a system as an encoding into logic of a graph characterized by a set of initial states, a set of failure states (where the property of interest is violated) and a transition relation, which describes the connections among states. Interpolation can be then used as an alternative to the expensive exact computation, step by step, of the sets of states which are reachable from the initial ones.

State-of-the-art procedures for interpolation in SAT and SMT generate interpolants basing on the structure of resolution proofs of unsatisfiability. An important aspect of the project is the investigation of transformation techniques for resolution proofs, aimed at reducing the size and modifying the topology, in order to obtain interpolants of better quality in several theories of interest.

Our current results include papers [1], [2], [3], [4] and the OpenSMT tool, the basic SMT-solving framework we use for both research and experimentation.

References