Re: FWD: Looking for comments: Verify telecommunications system

• To: dv@festival.ed.ac.uk
• Subject: Re: FWD: Looking for comments: Verify telecommunications system
• From: "Stephen J. Garland" <garland@larch.lcs.mit.edu>
• Date: Mon, 27 Feb 95 09:57:17 -0500
• Cc: larch-interest@pa.dec.com, dv@srv2.med.ed.ac.uk
• Delivery-Date: Mon, 27 Feb 95 07:07:19 -0800

     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.

• Prev: Dismay
• Next: larch prover and protocols
• Index: Larch archive index