Counterexample-guided prophecy for model checking modulo the theory of arrays
From MaRDI portal
Publication:2044196
DOI10.1007/978-3-030-72016-2_7zbMath1467.68089arXiv2101.06825OpenAlexW3148335769MaRDI QIDQ2044196
Oded Padon, Ahmed Irfan, Clark Barrett, Alberto Griggio, Makai Mann
Publication date: 4 August 2021
Full work available at URL: https://arxiv.org/abs/2101.06825
Related Items (5)
Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ \textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Synthesizing history and prophecy variables for symbolic model checking ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ Universal invariant checking of parametric systems with quantifier-free SMT reasoning
Cites Work
- Unnamed Item
- Unnamed Item
- SMT-based model checking for recursive programs
- The existence of refinement mappings
- Local proofs for global safety properties
- Cell morphing: from array programs to array-free Horn clauses
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Infinite-state invariant checking with IC3 and predicate abstraction
- Lazy Abstraction with Interpolants for Arrays
- Horn Clause Solvers for Program Verification
- Weakly Equivalent Arrays
- Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
- SAT-Based Model Checking without Unrolling
- Satisfiability Modulo Theories
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Booster: An Acceleration-Based Verification Framework for Array Programs
- Quantified Heap Invariants for Object-Oriented Programs
- Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
- Computer Aided Verification
- The MathSAT5 SMT Solver
- Quantified Invariant Generation Using an Interpolating Saturation Prover
- MCMT: A Model Checker Modulo Theories
- Verification, Model Checking, and Abstract Interpretation
- Eager abstraction for symbolic model checking
- Quantifiers on demand
This page was built for publication: Counterexample-guided prophecy for model checking modulo the theory of arrays
