Counterexample-Guided Model Synthesis
From MaRDI portal
Publication:3303898
DOI10.1007/978-3-662-54577-5_15zbMath1452.68122OpenAlexW2600774173MaRDI QIDQ3303898
Armin Biere, Mathias Preiner, Aina Niemetz
Publication date: 5 August 2020
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-662-54577-5_15
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Syntax-guided quantifier instantiation ⋮ On solving quantified bit-vector constraints using invertibility conditions
Uses Software
Cites Work
- Unnamed Item
- Complexity of fixed-size bit-vector logics
- Counterexample-guided quantifier instantiation for synthesis in SMT
- A layered algorithm for quantifier elimination from linear modular constraints
- Efficiently solving quantified bit-vector formulas
- Solving Quantified Bit-Vector Formulas Using Binary Decision Diagrams
- Automated Discovery of Simulation Between Programs
- Simplify: a theorem prover for program checking
- Ranking Function Synthesis for Bit-Vector Relations
- Constraint-Based Invariant Inference over Predicate Abstraction
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Exploiting Circuit Representations in QBF Solving
- From program verification to program synthesis
