Example IOA Programs

The following documents are mostly in the form of reports on the experiments carried out by group members. The full IOA code for the examples are included in the current software distribution under the Examples directory.

A Test for the IOA-Daikon Connection: Banking Examples in IOA presents a set of experiments done on examples from the paper Using I/O Automata for Developing Distributed Systems.
Steve Garland has written an IOA description of the LeLann-Chang-Roberts leader election algorithm.
Chris Luhrs is currently writing a collection of distributed network algorithms in IOA, designed to be used as test examples for various tools. Invariant and Simulation Relation Proofs for IOA Algorithms using LP details his proof of a distributed spanning tree algorithm using LP. Thoughts on LP contains his opinions and insights about using the Larch Prover.
Frits Vaandrager has posted examples of IOA specifications discussed during his course on Protocol Validation at the University of Nijmegen.

Return to IOA Homepage