Deciding Local Theory Extensions via E-matching

by Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, Thomas Wies
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.
Reference:
Deciding Local Theory Extensions via E-matching (Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, Thomas Wies), In Proceedings of the 27th International Conference on Computer Aided Verification (CAV ’15) (Daniel Kroening, Corina S. Puasuareanu, eds.), Springer, volume 9206, 2015. (San Francisco, CA)
Bibtex Entry:
@inproceedings{BRK+15,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/BRK+15.pdf",
  author    = "Kshitij Bansal and Andrew Reynolds and Tim King and Clark Barrett and Thomas Wies",
  title     = "Deciding Local Theory Extensions via {E}-matching",
  booktitle = "Proceedings of the 27th International Conference on Computer Aided Verification (CAV '15)",
  volume    = 9206,
  number    = 2,
  editor    = "Daniel Kroening and Corina S. Pu{a}su{a}reanu",
  pages     = "87--105",
  series    = "Lecture Notes in Computer Science",
  publisher = "Springer",
  month     = jul,
  year      = 2015,
  note      = "San Francisco, CA",
  category  = "Conference Publications",
  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."
}

Fork me on GitHub