Counterexample-guided quantifier instantiation for synthesis in SMT

DOI10.1007/978-3-319-21668-3_12zbMath1381.68059arXiv1502.04464OpenAlexW1912569824MaRDI QIDQ1702893

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

Publication date: 1 March 2018

Full work available at URL: https://arxiv.org/abs/1502.04464

Mathematics Subject Classification ID

Related Items (16)

Programmable program synthesis ⋮ Counterexample-guided partial bounding for recursive function synthesis ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Synthesising programs with non-trivial constants ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ Syntax-guided quantifier instantiation ⋮ Counterexample-Guided Model Synthesis ⋮ Scaling Enumerative Program Synthesis via Divide and Conquer ⋮ Refutation-based synthesis in SMT ⋮ Higher-order quantifier elimination, counter simulations and fault-tolerant systems ⋮ On solving quantified bit-vector constraints using invertibility conditions ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ Explaining AI decisions using efficient methods for learning sparse Boolean formulae ⋮ Scalable algorithms for abduction via enumerative syntax-guided synthesis ⋮ Verifying Whiley programs with Boogie ⋮ MedleySolver: online SMT algorithm selection

Uses Software

• SIMPLIFY
• StarExec
• CVC4
• TRANSIT

This page was built for publication: Counterexample-guided quantifier instantiation for synthesis in SMT