Counterexample-Guided Model Synthesis

DOI10.1007/978-3-662-54577-5_15MaRDI QIDQ3303898zbMATH OpenOpenAlexFDO

Authors Mathias Preiner, Aina Niemetz, Armin Biere

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Counterexample-guided synthesis of observation predicates
• Counterexample-Guided Assume-Guarantee Synthesis through Learning
• Counterexample guided inductive synthesis modulo theories
• Fundamental Approaches to Software Engineering
• Counterexample-guided abstraction refinement for symbolic model checking
• Counterexample-guided inductive synthesis for probabilistic systems

Cites work

• A layered algorithm for quantifier elimination from linear modular constraints
• Automated discovery of simulation between programs
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Complexity of fixed-size bit-vector logics
• Constraint-Based Invariant Inference over Predicate Abstraction
• Counterexample-guided quantifier instantiation for synthesis in SMT
• Efficiently solving quantified bit-vector formulas
• Exploiting circuit representations in QBF solving
• From program verification to program synthesis
• Handbook of automated reasoning. In 2 vols
• Ranking function synthesis for bit-vector relations
• Simplify: a theorem prover for program checking
• Solving quantified bit-vector formulas using binary decision diagrams

Cited in

(8)

• Counterexample-guided quantifier instantiation for synthesis in SMT
• On solving quantified bit-vector constraints using invertibility conditions
• Syntax-guided quantifier instantiation
• Syntax-guided synthesis for lemma generation in hardware model checking
• Synthesis of domain specific CNF encoders for bit-vector solvers
• Solving quantified bit-vectors using invertibility conditions
• Bitwuzla
• Truncating abstraction of bit-vector operations for BDD-based SMT solvers

Describes a project that uses

Uses Software

• Boolector
• Yices
• z3
• CVC4
• SMT-LIB
• SIMPLIFY
• Easychair
• TRANSIT

This page was built for publication: Counterexample-Guided Model Synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3303898)