Stephan Merz — some talks

Reduction Revisited: Verifying Round-Based Distributed Algorithms

(Invited talk at MPC/AMAST 2010, Québec, Canada, June 2010)

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.

The TLA+ Proof System

(Given at the Amir Pnueli Memorial Symposium, New York University, May 2010)

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.)

Refinement of events with permissions and obligations

Proposal of an extension of event systems by fairness conditions, obligations, interdictions, and permissions. The latter "deontic" properties are relevant in connection with work on information security (more specifically, access control). Whereas there are frameworks to represent such concepts, few formal development methods reflect them in their notions of correctness and refinement.

Modeling and Developing Systems Using TLA+

Material for a course on the TLA+ specification language, including the TLC model checker, given at a summer school in Rio Cuarto, Argentina.

Model Checking

with Javier Esparza

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)!