Publications Related to the IOA Language and Toolset

Stephen J. Garland and Nancy A. Lynch. "Using I/O automata for developing distributed systems," Foundations of Component-Based Systems, Gary T. Leavens and Murali Sitaraman, editors, Cambridge University Press, 2000, pages 285-312.
Abstract

An overview of the design of the IOA language and toolset. Includes an extended example of a toy distributed banking system.

Stephen J. Garland, Nancy A. Lynch, and Mandana Vaziri. IOA: a language for specifying, programming, and validating distributed systems, MIT Laboratory for Computer Science, 1997.
Paper

The reference manual for the IOA language. Gives a full description of the syntax and semantics of IOA.

Tsvetomir P. Petrov, Anna Pogosyants, Stephen J. Garland, Victor Luchangco, and Nancy A. Lynch. "Computer-assisted verification of an algorithm for concurrent timestamps," Formal Description Techniques IX: Theory, Applications, and Tools, Reinhard Gotzhein and Jan Bredereke, editors, Chapman and Hall, 1996, pages 29-44. (Proceedings of the FORTE/PSTV '96 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, Kaiserslautern, Germany, October 8-11, 1996.)
Abstract, Paper (pdf, compressed PostScript)

Describes an LP proof based on invariant assertions and simulation maps.

Victor Luchangco, Ekrem Söylemez, Stephen Garland, and Nancy Lynch. "Verifying timing properties of concurrent algorithms," FORTE '94: Seventh International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols, Berne, Switzerland, October 4-7, 1994, Chapman and Hall, pages 259-273.
Abstract

Describes an LP proof about timed automata. A future extension of the IOA Language may be based on the ideas in this paper.

Jørgen F. Søgaard-Andersen, Stephen J. Garland, John V. Guttag, Nancy A. Lynch, and Anya Pogosyants, "Computed-assisted simulation proofs," Computer-Aided Verification, Fifth International Conference, CAV '93, Elounda, Greece, June/July 1993, Lecture Notes in Computer Science 697, Costas Courcoubetis (editor), Springer-Verlag, pages 305-319.
Abstract

The first paper describing the use of LP to reason about input/output automata.