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

DOI10.46298/LMCS-18(3:26)2022MaRDI QIDQ5043584zbMATH OpenOpenAlexWikidataFDO

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)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

model checkingprophecy variablesquantified invariantsatisfiability modulo theoriestheory of arrays

Mathematics Subject Classification ID

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

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

• An axiomatic proof technique for parallel programs
• 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 abstraction refinement for symbolic model checking
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Decision procedures. An algorithmic point of view
• Eager abstraction for symbolic model checking
• Global guidance for local generalization in 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 53151 (Why is no real title available?)
• scientific article; zbMATH DE number 7453201 (Why is no real title available?)
• scientific article; zbMATH DE number 5194318 (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
• Quantifier-free interpolation of a theory of arrays
• Quantifiers on demand
• SAT-Based Model Checking without Unrolling
• Satisfiability modulo theories
• SMT-based model checking for recursive programs
• Temporal prophecy for proving temporal properties of infinite-state systems
• The MathSAT5 SMT solver
• Universal invariant checking of parametric systems with quantifier-free SMT reasoning
• Verification, Model Checking, and Abstract Interpretation
• Weakly equivalent arrays

Cited in

(2)

• Communicating Sequential Processes. The First 25 Years
• Synthesizing history and prophecy variables for symbolic model checking

Describes a project that uses

Uses Software

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

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)