Counterexample-guided quantifier instantiation for synthesis in SMT
From MaRDI portal
Publication:1702893
DOI10.1007/978-3-319-21668-3_12zbMATH Open1381.68059arXiv1502.04464OpenAlexW1912569824MaRDI QIDQ1702893FDOQ1702893
Authors: Andrew Reynolds, Morgan Deters, Viktor Kuncak, Cesare Tinelli, Clark Barrett 
Publication date: 1 March 2018
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.
Full work available at URL: https://arxiv.org/abs/1502.04464
Recommendations
Cited In (26)
- Higher-order quantifier elimination, counter simulations and fault-tolerant systems
- Invariant synthesis for incomplete verification engines
- Verifying Whiley programs with Boogie
- Synthesising programs with non-trivial constants
- Counterexample-guided partial bounding for recursive function synthesis
- Syntax-guided synthesis with quantitative syntactic objectives
- Programmable program synthesis
- Syntax-guided quantifier instantiation
- Syntax-guided synthesis for lemma generation in hardware model checking
- On solving quantified bit-vector constraints using invertibility conditions
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Scaling enumerative program synthesis via divide and conquer
- Refutation-based synthesis in SMT
- Identifying overly restrictive matching patterns in SMT-based program verifiers (extended version)
- Instrumenting a weakest precondition calculus for counterexample generation
- Satisfiability and synthesis modulo oracles
- Partial bounding for recursive function synthesis
- Datatypes with shared selectors
- Towards bit-width-independent proofs in SMT solvers
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Counterexample guided inductive synthesis modulo theories
- Explaining AI decisions using efficient methods for learning sparse Boolean formulae
- Counterexample-Guided Model Synthesis
- MedleySolver: online SMT algorithm selection
- Proving unrealizability for syntax-guided synthesis
- Scalable algorithms for abduction via enumerative syntax-guided synthesis
Uses Software
This page was built for publication: Counterexample-guided quantifier instantiation for synthesis in SMT
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1702893)
