Distributed State Space Exploration
From LRDE
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- 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 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.