Reachability programming in HOL98 using BDDs

DOI10.1007/3-540-44659-1_12MaRDI QIDQ2754043zbMATH OpenFDO

Authors Michael J. C. Gordon

Publication date 11 November 2001

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

Full work available at URL https://doi.org/10.1007/3-540-44659-1_12

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Symbolic computation and algebraic computation (68W30)

Recommendations

• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• scientific article; zbMATH DE number 2086515
• Symbolic reachability analysis based on SAT-solvers
• Reflecting BDDs in Coq
• Programming a symbolic model checker in a fully expansive theorem prover

Cited in

(5)

• Computer assisted reasoning. A Festschrift for Michael J. C. Gordon
• Proof Pearl: Revisiting the Mini-rubik in Coq
• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• LCF-style Platform based on Multiway Decision Graphs
• Providing a formal linkage between MDG and HOL

This page was built for publication: Reachability programming in HOL98 using BDDs

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