Satisfiability Modulo Software
Micha l Jan Moskal, Leszek M. Pacholski, Jan Moskal · 2009
Formal verification is the act of proving correctness of a hardware or software system using formal methods of mathematics. In the last decade formal hardware verification has seen an increasing usage of Satisfiability Modulo Theories (SMT) solvers. SMT solvers check satisfiability of first-order formulas, where certain symbols are interpreted according to background theories like integer or bit-vector arithmetic. Since the formulas used to encode correctness of hardware design are mostly quantifier-free, SMT solvers are built as theory-aware extensions of propositional satisfiability solvers. As a consequence, SMT solvers do not “naturally ” support quantified formulas, which are needed for verification of complex software systems. Thus, while SMT solvers are already an industrially viable tool for formal hardware verification, software applications are not as developed. This thesis focuses on both the software verification specific problems in the construction of SMT solvers, as well as SMT-specific parts of a software verification system. On the SMT side, we present algorithms for efficient non-ground reasoning through quantifier instantiation and techniques for proof generation and proof checking for quantifier-rich software verification problems. On the verification tool side, we present methods for transforming programs into formulas in a solver-friendly way, with particular emphasis on design of annotations guiding the SMT solver through the non-ground part of the problem. The theoretical developments presented here were experimentally validated in implementations of state-of-the-art tools: an SMT solver and a verifier for concurrent C programs.