Sciweavers

Share
ENTCS
2006

Distributed Symbolic Bounded Property Checking

10 years 11 months ago
Distributed Symbolic Bounded Property Checking
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. Key words: Verification, bounded model checking, property checking, binary decision diagrams, parallelization.
Pradeep Kumar Nalla, Roland J. Weiss, Prakash Moha
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Pradeep Kumar Nalla, Roland J. Weiss, Prakash Mohan Peranandam, Jürgen Ruf, Thomas Kropf, Wolfgang Rosenstiel
Comments (0)
books