Refutation-based synthesis in SMT

DOI10.1007/s10703-017-0270-2zbMath1427.68051OpenAlexW2589084440MaRDI QIDQ2280222

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

Publication date: 18 December 2019

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-017-0270-2

zbMATH Keywords

program synthesisautomated deductionsatisfiability modulo theories

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Special issue on syntax-guided synthesis preface ⋮ Automated repair for timed systems ⋮ Targeted configuration of an SMT solver ⋮ Defining behaviorizeable relations to enable inference in semi-automatic program synthesis

Uses Software

• Yices
• z3
• SIMPLIFY
• Nuprl
• StarExec
• CVC4
• Spacer
• TRANSIT
• Mjollnir
• RAReQS

Cites Work

• Unnamed Item
• Unnamed Item
• Synthesis of Reactive(1) designs
• SMT-based model checking for recursive programs
• Solving quantified linear arithmetic by counterexample-guided instantiation
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Efficiently solving quantified bit-vector formulas
• Solving QBF with Counterexample Guided Refinement
• Abstraction-Based Algorithm for 2QBF
• Towards Complete Reasoning about Axiomatic Specifications
• Program Synthesis Using Dual Interpretation
• Solving SAT and SAT Modulo Theories
• Simplify: a theorem prover for program checking
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Efficient E-Matching for SMT Solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• A Deductive Approach to Program Synthesis
• Quantifier Instantiation Techniques for Finite Model Finding in SMT
• Exploiting Symmetry in SMT Problems
• Theorem Proving in Higher Order Logics
• Verification, Model Checking, and Abstract Interpretation
• Linear Quantifier Elimination as an Abstract Decision Procedure

This page was built for publication: Refutation-based synthesis in SMT