Re: FWD: Looking for comments: Verify telecommunications system
You might want to take a look at the work we have been doing at MIT using
the Larch Prover to check proofs about concurrent algorithms that have been
formulated using the notion of an I/O automaton. Here are two recent papers:
Joergen F. Soegaard-Anderson, Stephen J. Garland, John V. Guttag, Nancy A.
Lynch, and Anna Pogosyants, ``Computed-assisted simulation proofs,'' in
Costas Courcoubetis, editor, Fifth Conference on Computer-Aided
Verification, Crete, June 1993. Springer-Verlag Lecture Notes in Computer
Science 697, pages 305-319.
Victor Luchangco, Ekrem Soylemez, Stephen J. Garland, and Nancy Lynch,
``Verifying timing properties of concurrent algorithms,'' FORTE'94:
Seventh International Conference on Formal Description Techniques, Berne,
Switzerland, October 4-7, 1994, Chapman and Hall.