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 is propositional logic; 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).

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, a SAT-Solver 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 symbolic 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 behavior of the system. 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 propositional interpolation generate interpolants based on the structure of resolution proofs of unsatisfiability. Interpolants are not unique, since (i) multiple proofs of unsatisfiability can exist for the same formula, and (ii) different interpolants can be obtained from the same proof. An important goal of this project is thus to investigate what characterizes good interpolants, and to develop new algorithms that guide their generation in order to improve the verification performance.

We are currently focusing on two features which are intuitively relevant to model checking, and for which preliminary evidence has been provided in the literature: logical strength and size. On one side, since interpolants are treated as overapproximations, a stronger or weaker interpolant affects verification in terms of a finer or coarser approximation; on the other side, interpolants are formulae that must be generated and stored, and might be used multiple times. Interpolants are generated from proofs of unsatisfiability, and smaller interpolants can be obtained by reducing the size of the proofs; a goal of this project is also the development of transformation algorithms for resolution proofs, including compression techniques that can be applied to yield more compact interpolants.

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

References