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

DOI10.1007/978-3-030-72016-2_7MaRDI QIDQ2044196zbMATH OpenOpenAlexFDO

Authors Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett

Publication date 4 August 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2101.06825

Mathematics Subject Classification ID

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

Abstract: We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction refinement scheme for the theory of arrays. Our framework can thus, in many cases, reduce inductive reasoning with quantifiers and arrays to quantifier-free and array-free reasoning. We evaluate the approach on a wide set of benchmarks from the literature. The results show that our implementation often outperforms state-of-the-art tools, demonstrating its practical potential.

Recommendations

• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Towards SMT Model Checking of Array-Based Systems
• MCMT: a model checker modulo theories
• Light-weight SMT-based model checking
• Thread-modular counterexample-guided abstraction refinement

Cites work

• Booster: an acceleration-based verification framework for array programs
• Cell morphing: from array programs to array-free Horn clauses
• Computer Aided Verification
• Computing small unsatisfiable cores in satisfiability modulo theories
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Eager abstraction for symbolic model checking
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 5613976 (Why is no real title available?)
• scientific article; zbMATH DE number 7453201 (Why is no real title available?)
• Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions
• Infinite-state invariant checking with IC3 and predicate abstraction
• Lazy abstraction with interpolants for arrays
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Local proofs for global safety properties
• MCMT: a model checker modulo theories
• Quantified Heap Invariants for Object-Oriented Programs
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• Quantifiers on demand
• SAT-Based Model Checking without Unrolling
• Satisfiability modulo theories
• SMT-based model checking for recursive programs
• The existence of refinement mappings
• The MathSAT5 SMT solver
• Verification, Model Checking, and Abstract Interpretation
• Weakly equivalent arrays

Cited in

(8)

• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• Towards SMT Model Checking of Array-Based Systems
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Communicating Sequential Processes. The First 25 Years
• Bounded model checking and induction: From refutation to verification (extended abstract, Category A)
• Synthesizing history and prophecy variables for symbolic model checking
• \textsc{Diffy}: inductive reasoning of array programs using difference invariants

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 Q2044196)