engleski

Parallel approaches to BDD manipulation

Symbolic model checking is an automatic method for system verification in which the system is given as a Binary Decision Diagram (BDD) encoded finite state machine. BDD is a common data structure for representation of mathematical objects. The main issue in symbolic model checking is a state explosion problem that restricts the verification domain. In this paper we present possibilities for the parallelization of BDD manipulation algorithms in order to enable verification of complex systems. We also demonstrate results of our parallel algorithm for computing BDD operations.

BDD ; formal methods ; symbolic model checking ; parallel algorithms ; formal verification

nije evidentirano