Programming a symbolic model checker in a fully expansive theorem prover
From MaRDI portal
Recommendations
Cited in
(18)- Formal verification of a partial-order reduction technique for model checking
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
- scientific article; zbMATH DE number 1670743 (Why is no real title available?)
- Model checking for symbolic-heap separation logic with inductive predicates
- Explicit-symbolic modelling for formal verification
- Simplify: a theorem prover for program checking
- scientific article; zbMATH DE number 1487865 (Why is no real title available?)
- scientific article; zbMATH DE number 1759597 (Why is no real title available?)
- Automatic verification of reduction techniques in higher order logic
- scientific article; zbMATH DE number 2086515 (Why is no real title available?)
- scientific article; zbMATH DE number 2102719 (Why is no real title available?)
- Programming Combinations of Deduction and BDD-based Symbolic Calculation
- LCF-style Platform based on Multiway Decision Graphs
- Proving the refuted: symbolic model checkers as proof generators
- Automated Technology for Verification and Analysis
- Relational and Kleene-Algebraic Methods in Computer Science
- Certifying phase abstraction
- Providing a formal linkage between MDG and HOL
This page was built for publication: Programming a symbolic model checker in a fully expansive theorem prover
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3559766)
