Article ID Journal Published Year Pages File Type
423281 Electronic Notes in Theoretical Computer Science 2006 17 Pages PDF
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