Counterexample-guided quantifier instantiation for synthesis in SMT
From MaRDI portal
Publication:1702893
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
This page was built for publication: Counterexample-guided quantifier instantiation for synthesis in SMT
