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 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.
Cite
CITATION STYLE
Søgaard-Andersen, J. F., Garland, S. J., Guttag, J. V., Lynch, N. A., & Pogosyants, A. (1993). Computer-assisted simulation proofs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 697 LNCS, pp. 305–319). Springer Verlag. https://doi.org/10.1007/3-540-56922-7_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
