Distributed State Space Exploration



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 structures, we 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.