Computer-Assisted Simulation Proofs

Abstract. 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 speci cation 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 speci cations for a communication protocol.

• Type: Conference
• Year: 1993
• Where: CAV
• Authors: Jørgen F. Søgaard-Andersen, Stephen J. Garland, John V. Guttag, Nancy A. Lynch, Anna Pogosyants
• Keywords: CAV 1993, Hardware, Proof Obligations, Scalable Approach, Speci Cations