Name
Abstract | ||
|---|---|---|
In this paper we describe an algorithm for distributed, BDD-based bounded property checking and its implementation in the verification tool SymC. The distributed algorithm verifies larger models and returns results faster than the sequential version. The core algorithm distributes partitions of the state set to computation nodes after reaching a threshold size. The nodes proceed with image computation on the nodes asynchronously. The main scalability problem of this scheme is the overlap of state set partitions. We present static and dynamic overlap reduction techniques. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.entcs.2005.10.018 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
reduction technique,property checking,parallelization,main scalability problem,core algorithm,bdd-based bounded property checking,symbolic bounded property checking,verification,returns result,binary decision diagrams,bounded model checking,image computation,nodes asynchronously,parallelization.,state set partition,algorithm verifies,larger model,binary decision diagram,distributed algorithm | Discrete mathematics,Model checking,Computer science,Theoretical computer science,Distributed algorithm,Computation,Bounded function,Scalability | Journal |
Volume | Issue | ISSN |
135 | 2 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
1 | 0.37 | 26 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pradeep K. Nalla | 1 | 16 | 1.82 |
| Roland J. Weiss | 2 | 11 | 4.81 |
| Prakash Mohan Peranandam | 3 | 7 | 2.64 |
| Jürgen Ruf | 4 | 122 | 23.04 |
| Thomas Kropf | 5 | 326 | 59.09 |
| Wolfgang Rosenstiel | 6 | 1462 | 212.32 |