Sciweavers

Share
ATVA
2007
Springer

Verifying Heap-Manipulating Programs in an SMT Framework

10 years 2 months ago
Verifying Heap-Manipulating Programs in an SMT Framework
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.
Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. H
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where ATVA
Authors Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti
Comments (0)
books