![](https://csd.cmu.edu/sites/default/files/styles/full_width_focal_point/public/graduate.png.webp?itok=Wsy3nMEH)
Anvesh Komuravelli
Thesis Title:
Compositional Verification with Abstraction, Learning, and SAT Solving
Degree Type:
Ph.D. in Computer Science
Advisor(s):
Edmund Clarke
Graduated:
May
2015
Abstract:
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
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
Keywords: Model checking, verification, proof, counterexample, satisfiability, SAT, SMT, oracle, abstraction, refinement, approximation, logic, quantifier elimination, decision procedure, program, software, loops, recursion, procedures, Z3, induction, safety, modular, compositional, invariant, interpolation, cegar, proof-based abstraction, symbolic, parallel, probability, transition system, simulation, active learning, undecidable
CMU-CS-15-102.pdf (1.73 MB) ( 228 pages)Copyright Notice