[Title] Towards Automatic Verification of Message-Passing Algorithms
[Speaker] Rotem Oshman (MIT)
[Place] 32-G631
[Time] 1:00PM - 2:30PM
[Date] Feb. 26th (Fri), 2010

[Abstract]
In this talk I will describe a project I worked on with Andy Drucker in last
term's Foundations of Software Analysis class. The goal of the project is to
obtain mechanically-verified proofs for a class of approximate agreement
algorithms running in networks of unbounded size.
Unbounded networks (and unbounded objects in general) present a challenge
for formal verification, because many automatic verification techniques
involve some form of exhaustive search. Recent advances allow automatic
proofs for shared-memory programs with unboundedly many threads, but we are
not aware of any corresponding techniques for message-passing systems of
unbounded size.
In this work we give a proof rule that can prove the correctness of
approximate agreement algorithms in unbounded networks. The user specifies
invariants that characterize the \emph{local} interactions of processes, and
the proof rule generalizes these to a \emph{global} proof of correctness. We
define a notion we call \emph{causal diameter}, which captures the time
required for information to spread through the network, and use it to reason
in a unified way about systems with various types of node and edge failures.
Using the proof rule and the Z3 SMT solver we were able to verify two simple
examples: the well-known FloodMin algorithm for consensus in the presence of
crash failures, and a global clock synchronization algorithm that works in
static or dynamic graphs that always remain connected. In both cases the
property proven is parameterized by the diameter of the system. We hope to
extend the approach to reason about other, more complex classes of
algorithms.