Anvesh Komuravelli

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 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 parallel 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.

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