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.