Reflecting BDDs in Coq

DOI10.1007/3-540-44464-5_13MaRDI QIDQ2766536zbMATH OpenFDO

Authors Kumar Neeraj Verma, Jean Goubault-Larrecq, Sanjiva Prasad, S. Arun-Kumar

Publication date 8 July 2002

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

Full work available at URL https://doi.org/10.1007/3-540-44464-5_13

Mathematics Subject Classification ID

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

Recommendations

• Implementing hash-consed structures in Coq
• Bddl: A Type System for Binary Decision Diagrams
• scientific article; zbMATH DE number 2086515
• Extending Coq with Imperative Features and Its Application to SAT Verification
• Programming Combinations of Deduction and BDD-based Symbolic Calculation

Cited in

(13)

• Proof reflection in Coq
• Implementing and reasoning about hash-consed data structures in Coq
• Reachability programming in HOL98 using BDDs
• Coquet: a Coq library for verifying hardware
• Extracting a DPLL algorithm
• Formalizing the Logic-Automaton Connection
• LCF-Style Propositional Simplification with BDDs and SAT Solvers
• Memoization
• scientific article; zbMATH DE number 2086515 (Why is no real title available?)
• Programming Combinations of Deduction and BDD-based Symbolic Calculation
• Implementing hash-consed structures in Coq
• Formalized proof systems for propositional logic
• Bddl: A Type System for Binary Decision Diagrams

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Reflecting BDDs in Coq

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