Paper Info
Title
Verifying heap-manipulating programs in an SMT framework
Abstract
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.
Year
DOI
Venue
2007
10.1007/978-3-540-75596-8_18
ATVA
Keywords
Field
DocType
boolean satisfiability solvers,available smt solver,available smt solvers,general software,smt framework,decision procedure,automated decision procedure,unbounded heap reachability,extended smt solver,heap-manipulating program,automated software verification,unbounded reachability,software verification,satisfiability modulo theories,data structure
Data structure,Programming language,Predicate abstraction,Computer science,Boolean satisfiability problem,Theoretical computer science,Heap (data structure),Reachability,Software,Satisfiability modulo theories,Software verification
Conference
Volume
ISSN
ISBN
4762
0302-9743
3-540-75595-0
Citations 
PageRank 
References 
14
0.61
31
Authors
4
Name
Order
Citations
PageRank
Zvonimir Rakamarić11357.41
Roberto Bruttomesso246329.46
Alan J. Hu31427148.29
Alessandro Cimatti45064323.15