Book chapter
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT
Computer Aided Verification, pp.198-216
Lecture Notes in Computer Science, Springer International Publishing
07/14/2015
DOI: 10.1007/978-3-319-21668-3_12
Abstract
We introduce the first program synthesis engine implemented inside an SMT solver. We present an approach that extracts solution functions from unsatisfiability proofs of the negated form of synthesis conjectures. We also discuss novel counterexample-guided techniques for quantifier instantiation that we use to make finding such proofs practically feasible. A particularly important class of specifications are single-invocation properties, for which we present a dedicated algorithm. To support syntax restrictions on generated solutions, our approach can transform a solution found without restrictions into the desired syntactic form. As an alternative, we show how to use evaluation function axioms to embed syntactic restrictions into constraints over algebraic datatypes, and then use an algebraic datatype decision procedure to drive synthesis. Our experimental evaluation on syntax-guided synthesis benchmarks shows that our implementation in the CVC4 SMT solver is competitive with state-of-the-art tools for synthesis.
Details
- Title: Subtitle
- Counterexample-Guided Quantifier Instantiation for Synthesis in SMT
- Creators
- Andrew Reynolds - École Polytechnique Fédérale de LausanneMorgan Deters - New York UniversityViktor Kuncak - École Polytechnique Fédérale de LausanneCesare Tinelli - University of IowaClark Barrett - New York University
- Resource Type
- Book chapter
- Publication Details
- Computer Aided Verification, pp.198-216
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-21668-3_12
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 07/14/2015
- Academic Unit
- Computer Science
- Record Identifier
- 9984259487502771
Metrics
9 Record Views