Formal verification of simulations between I/O automata Andrej Bogdanov Master of Engineering Thesis July, 2001

thesis.pdf: Formal verification of simulations between I/O automata Abstract: This thesis presents a tool for validating descriptions of distributed algorithms in the IOA language using an interactive theorem prover. The tool translates IOA programs into Larch Shared Language specifications in a style which is suitable for formal reasoning. The framework supports two common strategies for establishing the correctness of distributed algorithms: Invariants and simulation relations. These strategies are used to verify three distributed data management algorithms: A strong caching algorithm, a majority voting algorithm and Lamport's replicated state machine algorithm.

proofs.tar.gz: This file contains the Larch proof scripts for the invariants and forward simulation relations in Chapters 5, 6 and 7. You will need a copy of the Larch Prover release 3.1b to run these scripts. Syntax: make [cache | voting | synch]