Name
Abstract | ||
|---|---|---|
We describe an implementation and a proof of correctness of binary decision diagrams (BDDs), completely formalized in Coq. This allows us to run BDD-based algorithms inside Coq and paves the way for a smooth integration of symbolic model checking in the Coq proof assistant by using reflection. It also gives us, by Coq's extraction mechanism, certified BDD algorithms implemented in Caml. We also implement and prove correct a garbage collector for our implementation of BDDs inside Coq. Our experiments show that this approach works in practice, and is able to solve both relatively hard propositional problems and actual industrial hardware verification tasks. |
Year | Venue | Keywords |
|---|---|---|
2000 | ASIAN | binary decision diagram,hard propositional problem,actual industrial hardware verification,garbage collector,extraction mechanism,approach work,certified bdd,bdd-based algorithm,smooth integration,coq proof assistant,reflection,proof,extraction,caml |
Field | DocType | Volume |
Boolean function,Model checking,Programming language,Computer science,Correctness,Propositional calculus,Binary decision diagram,Theoretical computer science,Garbage collection,Boolean expression,Proof assistant | Conference | 1961 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-41428-2 | 18 |
PageRank | References | Authors |
0.97 | 16 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kumar Neeraj Verma | 1 | 171 | 8.87 |
| Jean Goubault-Larrecq | 2 | 582 | 40.90 |
| Sanjiva Prasad | 3 | 301 | 40.04 |
| S. Arun-Kumar | 4 | 48 | 4.95 |