Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
From MaRDI portal
Publication:5043584
DOI10.46298/LMCS-18(3:26)2022OpenAlexW4294598978WikidataQ124985757 ScholiaQ124985757MaRDI QIDQ5043584FDOQ5043584
Authors: Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett 
Publication date: 6 October 2022
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2101.06825
Recommendations
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Counterexample guided inductive synthesis modulo theories
- A proof theory for model checking: an extended abstract
- Counterexample-guided abstraction refinement for symbolic model checking
- A proof theory for model checking
- Compositional model checking with incremental counter-example construction
- Model Checking Recursive Programs with Exact Predicate Abstraction
- Counterexample-preserving reduction for symbolic model checking
- Counterexample-preserving reduction for symbolic model checking
Cites Work
- The MathSAT5 SMT solver
- Booster: an acceleration-based verification framework for array programs
- Counterexample-guided abstraction refinement for symbolic model checking
- Title not available (Why is that?)
- Computing small unsatisfiable cores in satisfiability modulo theories
- Quantified Heap Invariants for Object-Oriented Programs
- Quantifier-free interpolation of a theory of arrays
- Lazy abstraction with interpolants for arrays
- SAT-Based Model Checking without Unrolling
- Satisfiability modulo theories
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Title not available (Why is that?)
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- MCMT: a model checker modulo theories
- Verification, Model Checking, and Abstract Interpretation
- An axiomatic proof technique for parallel programs
- Infinite-state invariant checking with IC3 and predicate abstraction
- Title not available (Why is that?)
- Computer Aided Verification
- SMT-based model checking for recursive programs
- Decision procedures. An algorithmic point of view
- Cell morphing: from array programs to array-free Horn clauses
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- Horn clause solvers for program verification
- Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
- Quantifiers on demand
- Local proofs for global safety properties
- Eager abstraction for symbolic model checking
- Weakly equivalent arrays
- Title not available (Why is that?)
- Temporal prophecy for proving temporal properties of infinite-state systems
- Global guidance for local generalization in model checking
Cited In (2)
Uses Software
This page was built for publication: Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5043584)
