Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
423281 | Electronic Notes in Theoretical Computer Science | 2006 | 17 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics