Synthesizing history and prophecy variables for symbolic model checking

DOI10.1007/978-3-031-24950-1_15zbMath1529.68166OpenAlexW4316662619MaRDI QIDQ6174405

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

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• SMT-based model checking for recursive programs
• The existence of refinement mappings
• Cell morphing: from array programs to array-free Horn clauses
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• An interpolating theorem prover
• Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
• Property-Directed Inference of Universal Invariants or Proving Their Absence
• Abstractions from proofs
• Simplify: a theorem prover for program checking
• Verifying properties of parallel programs
• Infinite-State Liveness-to-Safety via Implicit Abstraction and Well-Founded Relations
• Formal Methods in Computer-Aided Design
• Verification, Model Checking, and Abstract Interpretation
• Eager abstraction for symbolic model checking
• Quantifiers on demand
• Quantified invariants via syntax-guided synthesis

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