Name
Abstract | ||
|---|---|---|
We present a study of the computational aspects of model checking based on binary decision diagrams (BDDs). By using a trace-based evaluation framework, we are able to generate realistic benchmarks and perform this evaluation collaboratively across several different BDD packages. This collaboration has resulted in significant performance improvements and in the discovery of several interesting characteristics of model checking computations. One of the main conclusions of this work is that the BDD computations in model checking and in building BDDs for the outputs of combinational circuits have fundamentally different performance characteristics. The systematic evaluation has also uncovered several open issues that suggest new research directions. We hope that the evaluation methodology used in this study will help lay the foundation for future evaluation of BDD-based algorithms. |
Year | Venue | Keywords |
|---|---|---|
1998 | FMCAD | systematic evaluation,model checking computation,performance study,different bdd package,evaluation methodology,model checking,trace-based evaluation framework,different performance characteristic,bdd computation,future evaluation,evaluation collaboratively,bdd-based model checking,binary decision diagram,combinational circuit |
Field | DocType | ISBN |
Graph theory,Model checking,Computer science,CPU cache,Binary decision diagram,Directed acyclic graph,Combinational logic,Theoretical computer science,Finite-state machine,Garbage collection | Conference | 3-540-65191-8 |
Citations | PageRank | References |
36 | 1.95 | 15 |
Authors | ||
8 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bwolen Yang | 1 | 123 | 9.89 |
| Randal E. Bryant | 2 | 9204 | 1194.64 |
| David R. O'hallaron | 3 | 1243 | 126.28 |
| Armin Biere | 4 | 4106 | 245.11 |
| Olivier Coudert | 5 | 665 | 104.87 |
| Geert Janssen | 6 | 127 | 8.90 |
| Rajeev K. Ranjan | 7 | 968 | 79.15 |
| Fabio Somenzi | 8 | 3394 | 302.47 |