Distributed State Space Exploration

Authors

Paul Guénézan

Type

techreport

Year

2019

Number

1904

Abstract

In the model checking field, the data structures used to represent a given program can't be stored in memory due to combinatorial explosion. To speed up the exploration of such large data structureswe can use parallel or distributed algorithms. In this report, we present an implemention of a distributed state space exploration algorithm proposed by Camille Coti in "One-Sided Communications for more Efficient Parallel State Space Exploration over RDMA Clusters". We compare it against a synchronous algorithm and an asynchronous algorithm using threads to communicate with the same machine. We give benchmarks of all these algorithms using the BEEN benchmark.