Parameterized Verification of Round-Based Shared-Memory Systems

We consider parameterized verification problems for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm introduced by Aspnes, we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. Verification algorithms thus needs to manage both sources of infinity. In this setting, we study several verification problems, among which safety (the error state cannot be reached) or inevitability (the error state cannot be avoided). This a joint work with Nathalie Bertrand, Nicolas Markey and Ocan Sankur.

Authors

• Nicolas Waldburger

Keywords

No keywords are indexed for this paper.