“Computed-assisted simulation proofs”

Jörgen F. Sögaard-Anderson, Stephen J. Garland, John V. Guttag, Nancy A. Lynch, and Anya Pogosyants

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

This paper presents a scalable approach to reasoning formally about distributed algorithms. It uses results about I/O automata to extract a set of proof obligations for showing that the behaviors of one algorithm are among those of another, and it uses the Larch tools for specification and deduction to discharge these obligations in a natural and easy-to-read fashion. The approach is demonstrated by proving the behavior equivalence of two high-level specifications for a communication protocol.

Back to Publications of Stephen J. Garland