CMU-CS-15-102 Computer Science Department School of Computer Science, Carnegie Mellon University
Compositional Verification with Anvesh Komuravelli May 2015 Ph.D. Thesis
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 228 pages
Thesis Committee:
Frank Pfenning, Head, Computer Science Department
| |
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |