Distributed algorithms are often quite subtle, in the way they operate and in the assumptions they make. Formal verification is therefore crucial in distributed computing. To facilitate their design and understanding, many existing distributed algorithms are structured in rounds: each process first sends messages, then receives messages from other processes, and finally makes a local state transition. However, existing formal models of distributed algorithms do not take advantage of this structure, but are based on a fine-grained description of systems whose individual processes are represented by communicating state machines.
Reduction theorems for concurrent and distributed algorithm have been studied since Lipton's seminal paper in 1975. Broadly speaking, they aim at pretending that certain sequences of events happen indivisibly, thus allowing verification to be carried out over coarser-grained models of algorithms and systems. We revisit this line of research and contribute a reduction theorem for distributed algorithms that are organized in communication-closed rounds, demonstrating its benefits on the verification of several consensus algorithms using model checking and theorem proving.
Joint work with Bernadette Charron-Bost, CNRS \& LIX, Palaiseau, France.
Reflecting on some of Pnueli's ideas for deductive program verification, this talk presents the main ideas underlying the TLA+ Proof System, released a few weeks prior to the event.
(Joint work with Kaustuv Chaudhuri, Damien Doligez, and Leslie Lamport at the INRIA-Microsoft Joint Centre.)
A 6-hour tutorial covering basic model checking techniques as well as some more advanced topics (abstraction, infinite-state model checking). The talk was given at the Petri Net Conference 2001.
Here comes the time warp: Javier gave a similar tutorial at the same conference a year later (though at the other end of the world)!