Sciweavers

Share
CAV
2015
Springer

Deciding Local Theory Extensions via E-matching

3 years 7 months ago
Deciding Local Theory Extensions via E-matching
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 ...
Kshitij Bansal, Andrew Reynolds, Tim King 0001, Cl
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CAV
Authors Kshitij Bansal, Andrew Reynolds, Tim King 0001, Clark W. Barrett, Thomas Wies
Comments (0)
books