Counterexample-guided prophecy for model checking modulo the theory of arrays

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

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

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