In symbolic model checking, Binary Decision Diagrams (BDDs) are often used to represent states of a system in a compressed way. By using reachability analysis the system's entire state space can be explored. However, even with symbolic representation models can grow exponentially during an analysis such that they do not fit in a single machine's working memory. Both multi-core and distributed reachability algorithms exist, but the combination of both is still uncommon.

In this work we present a design for multi-core distributed reachability analysis. Our work is based on the multi-core model checking tool Sylvan and combines this with a BDD partitioning approach. As network traffic is one of the bottlenecks that are often reported in distributed reachability designs, we tried to minimize communication between machines.

Our benchmark results show that our current design does not fully utilize available hardware capacity, but nevertheless our implementation was able to achieve speedups up to 29 compared to a linear execution and up to 5.3 compared to an existing multi-core distributed analysis tool.