Deciding Unbounded Heaps in an SMT Framework

Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti. 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), Berlin, Germany. (Presentation-only paper.)
[pdf] [slides]

Abstract: Satisfiability Modulo Theories (SMT) solvers have had great success in many different applications. The main reasons for this success are their efficiency and their support for the diverse theories that are required in different domains. Software verification has been a promising domain for SMT solvers, but verifying general software requires reasoning about unbounded linked heap data structures, including a theory that supports unbounded reachability. So far, none of the available SMT solvers supports such a theory. In this paper, we present our experience with integrating 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.