Synthesizing history and prophecy variables for symbolic model checking
From MaRDI portal
Publication:6174405
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
Cites work
- scientific article; zbMATH DE number 1701752 (Why is no real title available?)
- scientific article; zbMATH DE number 1956591 (Why is no real title available?)
- scientific article; zbMATH DE number 1852158 (Why is no real title available?)
- scientific article; zbMATH DE number 7453201 (Why is no real title available?)
- Abstractions from proofs
- An interpolating theorem prover
- Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
- Cell morphing: from array programs to array-free Horn clauses
- Counterexample-guided prophecy for model checking modulo the theory of arrays
- Eager abstraction for symbolic model checking
- Formal Methods in Computer-Aided Design
- Infinite-state liveness-to-safety via implicit abstraction and well-founded relations
- Property-directed inference of universal invariants or proving their absence
- Quantified invariants via syntax-guided synthesis
- Quantifiers on demand
- SMT-based model checking for recursive programs
- Simplify: a theorem prover for program checking
- The existence of refinement mappings
- Verification, Model Checking, and Abstract Interpretation
- Verifying properties of parallel programs
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)
