Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays

DOI10.46298/lmcs-18(3:26)2022OpenAlexW4294598978WikidataQ124985757 ScholiaQ124985757MaRDI QIDQ5043584

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

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

zbMATH Keywords

model checkingsatisfiability modulo theoriesprophecy variablesquantified invarianttheory of arrays

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Uses Software

• VAMPIRE
• SMT-LIB
• z3
• KRATOS
• CVC4
• Mcmt
• SeaHorn
• Spacer
• GitHub
• CTIGAR
• Booster

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• SMT-based model checking for recursive programs
• Decision procedures. An algorithmic point of view
• Local proofs for global safety properties
• An axiomatic proof technique for parallel programs
• 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
• Temporal prophecy for proving temporal properties of infinite-state systems
• Global guidance for local generalization in model checking
• Infinite-state invariant checking with IC3 and predicate abstraction
• Quantifier-Free Interpolation of a Theory of Arrays
• 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
• Counterexample-guided abstraction refinement for symbolic model checking
• 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