TY - GEN
T1 - Deciding local theory extensions via E-matching
AU - Bansal, Kshitij
AU - Reynolds, Andrew
AU - King, Tim
AU - Barrett, Clark
AU - Wies, Thomas
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84951005647&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84951005647&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-21668-3_6
DO - 10.1007/978-3-319-21668-3_6
M3 - Conference contribution
AN - SCOPUS:84951005647
SN - 9783319216676
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 87
EP - 105
BT - Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings
A2 - Păsăreanu, Corina S.
A2 - Kroening, Daniel
PB - Springer Verlag
T2 - 27th International Conference on Computer Aided Verification, CAV 2015
Y2 - 18 July 2015 through 24 July 2015
ER -