Paper Info
Title
Deciding Local Theory Extensions Via E-Matching
Abstract
Satisfiability Modulo Theories (SMT) solvers incorporate decision procedures for theories of data types that commonly occur in software. This makes them important tools for automating verification problems. A limitation frequently encountered is that verification problems are often not fully expressible in the theories supported natively by the solvers. Many solvers allow the specification of application-specific theories as quantified axioms, but their handling is incomplete outside of narrow special cases.In this work, we show how SMT solvers can be used to obtain complete decision procedures for local theory extensions, an important class of theories that are decidable using finite instantiation of axioms. We present an algorithm that uses E-matching to generate instances incrementally during the search, significantly reducing the number of generated instances compared to eager instantiation strategies. We have used two SMT solvers to implement this algorithm and conducted an extensive experimental evaluation on benchmarks derived from verification conditions for heap-manipulating programs. We believe that our results are of interest to both the users of SMT solvers as well as their developers.
Year
DOI
Venue
2015
10.1007/978-3-319-21668-3_6
COMPUTER AIDED VERIFICATION, CAV 2015, PT II
Field
DocType
Volume
Discrete mathematics,Programming language,Axiom,Computer science,Algorithm,Theoretical computer science,Software,Data type,Satisfiability modulo theories
Journal
9207
ISSN
Citations 
PageRank 
0302-9743
7
0.43
References 
Authors
24
5
Name
Order
Citations
PageRank
kshitij bansal1172.97
Andrew Reynolds2574.96
Tim King 00013302.51
Clark Barrett41268108.65
Thomas Wies551528.26