Automatic parameterized verification of distributed algorithms

When manually verifying safety and liveness properties of distributed systems composed of n processes, there is often some inductive invariant assertion that is shown to hold for all n processes, or n is chosen arbitrarily. This enables verification of the desired properties regardless of the number of participating processes. How can such manual methods be automated? This talk will focus on automated methods to solve the following formalization of the problem: given an automaton A, decide whether some temporal logic property holds when n copies of A are composed together. In general, this problem is undecidable even for finite state machines, but under various restrictions, even infinite state models such as timed automata have decidable solutions, albeit many of the methods can only be applied for safety and not liveness properties. This survey talk will cover some techniques from the software verification and model checking communities used to solve this problem (when possible) under different automata models. Several case study systems - such as cache coherence protocols and mutual exclusion algorithms - that have been automatically verified in this manner will be described.