Verifying Heap-Manipulating Programs in an SMT Framework

Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, and Alessandro Cimatti

Automated Technology for Verification and Analysis (ATVA), 2007.

Automated software verification has made great progress recently, and a key
enabler of this progress has been the advances in efficient, automated decision
procedures suitable for verification (Boolean satisfiability solvers and
satisfiability-modulo-theories (SMT) solvers).  Verifying general software,
however, requires reasoning about unbounded, linked, heap-allocated data
structures, which in turn motivates the need for a logical theory for such
structures that includes unbounded reachability.  So far, none of the available
SMT solvers supports such a theory.  In this paper, we present our integration
of a decision procedure that supports unbounded heap reachability into an
available SMT solver.  Using the extended SMT solver, we can efficiently verify
examples of heap-manipulating programs that we could not verify before.