Deciding local theory extensions via E-matching

Kshitij Bansal, Andrew Reynolds, Tim King, Clark Barrett, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 27th International Conference, CAV 2015, Proceedings
PublisherSpringer Verlag
Pages87-105
Number of pages19
Volume9207
ISBN (Print)9783319216676
DOIs
StatePublished - 2015
Event27th International Conference on Computer Aided Verification, CAV 2015 - San Francisco, United States
Duration: Jul 18 2015Jul 24 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9207
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other27th International Conference on Computer Aided Verification, CAV 2015
CountryUnited States
CitySan Francisco
Period7/18/157/24/15

Fingerprint

Extension Theory
Modulo
Decision Procedures
Axioms
Specifications
Heap
Experimental Evaluation
Benchmark
Specification
Software

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Bansal, K., Reynolds, A., King, T., Barrett, C., & Wies, T. (2015). Deciding local theory extensions via E-matching. In Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings (Vol. 9207, pp. 87-105). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9207). Springer Verlag. https://doi.org/10.1007/978-3-319-21668-3_6

Deciding local theory extensions via E-matching. / Bansal, Kshitij; Reynolds, Andrew; King, Tim; Barrett, Clark; Wies, Thomas.

Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings. Vol. 9207 Springer Verlag, 2015. p. 87-105 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9207).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Bansal, K, Reynolds, A, King, T, Barrett, C & Wies, T 2015, Deciding local theory extensions via E-matching. in Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings. vol. 9207, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9207, Springer Verlag, pp. 87-105, 27th International Conference on Computer Aided Verification, CAV 2015, San Francisco, United States, 7/18/15. https://doi.org/10.1007/978-3-319-21668-3_6
Bansal K, Reynolds A, King T, Barrett C, Wies T. Deciding local theory extensions via E-matching. In Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings. Vol. 9207. Springer Verlag. 2015. p. 87-105. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-21668-3_6
Bansal, Kshitij ; Reynolds, Andrew ; King, Tim ; Barrett, Clark ; Wies, Thomas. / Deciding local theory extensions via E-matching. Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings. Vol. 9207 Springer Verlag, 2015. pp. 87-105 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{4f710879e6f248c69661f26dd1ca0b72,
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.",
author = "Kshitij Bansal and Andrew Reynolds and Tim King and Clark Barrett and Thomas Wies",
year = "2015",
doi = "10.1007/978-3-319-21668-3_6",
language = "English (US)",
isbn = "9783319216676",
volume = "9207",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "87--105",
booktitle = "Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings",

}

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

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

VL - 9207

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

PB - Springer Verlag

ER -