Counterexample-guided quantifier instantiation for synthesis in SMT

Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark Barrett

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

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 27th International Conference, CAV 2015, Proceedings
EditorsCorina S. Păsăreanu, Daniel Kroening
PublisherSpringer Verlag
Pages198-216
Number of pages19
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)0302-9743
ISSN (Electronic)1611-3349

Other

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Counterexample-guided quantifier instantiation for synthesis in SMT'. Together they form a unique fingerprint.

Cite this