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 convegence 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. For probabilistic transition systems with multiple parall el components, the number of states of a system can grow exponentially in the number of components (the well-known state-space explosion problem). For these systems, we develop the first compositional algorithms for checking simulation conform ance. We follow an assume-guarantee style reasoning and establish theoretical bounds on the learnability of an intermediate assumption of the least number of states from positive and negative examples. We also develop a practical algorithm based on abstraction refinement. Using a Java implementation of the latter, we show practical advantage over monolithic verification.

228 pages

Thesis Committee:
Edmund M. Clarke (Chair)
Jonathan Aldrich
Frank Pfenning
Aarti Gupta (Princeton University)
Kenneth L. McMillan (Microsoft Research)
Corina S. Pasareanu (NASA Ames/CMU Silicon Valley)

Frank Pfenning, Head, Computer Science Department
Andrew W. Moore, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu