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.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Pradeep Kumar Nalla, Roland J. Weiss, Prakash Mohan Peranandam, Jürgen Ruf, Thomas Kropf, Wolfgang Rosenstiel
• Keywords: Algorithm, Checking, ENTCS 2006, Verification Tool Symc