Distributed Binary Decision Diagrams for Symbolic Reachability

Wytse Oortwijn, Tom van Dijk, Jaco van de Pol

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    8 Citations (Scopus)
    13 Downloads (Pure)


    Decision diagrams are used in symbolic verification to concisely represent state spaces. A crucial symbolic verification algorithm is reachability: systematically exploring all reachable system states. Although both parallel and distributed reachability algorithms exist, a combined solution is relatively unexplored. This paper contributes BDD-based reachability algorithms targeting compute clusters: high-performance networks of multi-core machines. The proposed algorithms may use the entire memory of every machine, allowing larger models to be processed while increasing performance by using all available computational power. To do this effectively, a distributed hash table, cluster-based work stealing algorithms, and several caching structures have been designed that all utilise the newest networking technology. The approach is evaluated extensively on a large collection of models, thereby demonstrating speedups up to 51,1x with 32 machines. The proposed algorithms not only benefit from the large amounts of available memory on compute clusters, but also from all available computational resources.
    Original languageEnglish
    Title of host publicationSPIN 2017 Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software
    PublisherAssociation for Computing Machinery
    Number of pages10
    ISBN (Print)978-1-4503-5077-8
    Publication statusPublished - Jul 2017
    Event24th International SPIN Symposium 2017: Model Checking of Software - University of California, Santa Barbara, United States
    Duration: 13 Jul 201714 Jul 2017
    Conference number: 24


    Conference24th International SPIN Symposium 2017
    Abbreviated titleSPIN 2017
    Country/TerritoryUnited States
    CitySanta Barbara
    Internet address


    • Symbolic model checking
    • parallel computing
    • distributed computing
    • high-performance computing
    • reachability analysis


    Dive into the research topics of 'Distributed Binary Decision Diagrams for Symbolic Reachability'. Together they form a unique fingerprint.

    Cite this