Synthesizing history and prophecy variables for symbolic model checking

DOI10.1007/978-3-031-24950-1_15zbMATH Open1529.68166OpenAlexW4316662619MaRDI QIDQ6174405FDOQ6174405

Authors: Cole Vick, K. L. McMillan 

Publication date: 17 August 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-24950-1_15

Recommendations

• A structural approach to prophecy variables
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Goal-directed invariant synthesis for model checking modulo theories
• Formal Techniques for Networked and Distributed Systems - FORTE 2005

Mathematics Subject Classification ID

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

Cites Work

• Simplify: a theorem prover for program checking
• Title not available (Why is that?)
• The existence of refinement mappings
• Verifying properties of parallel programs
• An interpolating theorem prover
• Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
• Abstractions from proofs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Verification, Model Checking, and Abstract Interpretation
• Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
• SMT-based model checking for recursive programs
• Cell morphing: from array programs to array-free Horn clauses
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Quantifiers on demand
• Quantified invariants via syntax-guided synthesis
• Formal Methods in Computer-Aided Design
• Eager abstraction for symbolic model checking
• Title not available (Why is that?)
• Property-directed inference of universal invariants or proving their absence

Cited In (1)

• Invariant checking for SMT-based systems with quantifiers

This page was built for publication: Synthesizing history and prophecy variables for symbolic model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174405)