Treffer: Compositional Verification with Abstraction, Learning, and SAT Solving

Compositional reasoning is an approach for scaling model checking to complex computer systems, where a given property of a system is decomposed into properties of small parts of the system. The key difficulty with compositional reasoning is in automatically coming up with sufficient decompositions of global properties into local properties. This thesis develops efficient compositional algorithms for safety of a) sequential recursive programs, using solvers for SAT and SAT modulo theories (SMT) and b) parallel, finite-state probabilistic systems. These algorithms result in significant improvements over the state-of-the-art, both in theory and in practice. For SAT-based verification of sequential programs, monolithic techniques based on Bounded Model Checking (BMC) iteratively check satisfiability of formulas whose size can grow exponentially in the input size of the program. While safety can be decided in time polynomial in the number of states, existing SAT-based algorithms do not have such guarantees. We develop a compositional SAT-based algorithm that maintains and utilizes under- and over-approximations of the behavior of procedures. While addressing the above complexity problem, the algorithm also extends to realistic programs that involve arithmetic operations using oracles for SMT. In order to improve practical convergence of the iterative approach for SMT-based verification, we also develop a new mechanism for automatic abstraction refinement of the input program. This combines ideas from Proof Based Abstraction (PBA) and CounterExample Guided Abstraction Refinement (CEGAR) in the literature. We describe Spacer (software Proof-based Abstraction with CounterExample- based Refinement) a tool that implements the above algorithms, using which we show significant advantages on realistic benchmarks. ; Sponsored in part by USAF and DARPA, grant no. F8721-05-C-0003 and ONR, grant no. N00014-10-1-0188.