src/HOLCF/IOA/README.html
author wenzelm
Wed May 21 17:13:00 1997 +0200 (1997-05-21)
changeset 3279 815ef5848324
parent 3071 981258186b71
child 5138 b02dfb930bd9
permissions -rw-r--r--
tuned all READMEs;
     1 <HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
     2 
     3 <H3>IOA: A formalization of I/O automata in HOLCF</H3>
     4 
     5 Author:     Olaf M&uuml;ller<BR>
     6 Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
     7 
     8 The distribution contains:
     9 <UL>
    10   <li> A semantic model of the meta theory of I/O automata including proofs for the refinement notion
    11        and the compositionality of the model. For details see: <BR>
    12        Olaf M&uuml;ller and Tobias Nipkow,
    13        <A HREF="http://www4.informatik.tu-muenchen.de/papers/tapsoft_mueller_1997_Conference.html">Traces of I/O Automata in Isabelle/HOLCF</A>.
    14 In <i> TAPSOFT'97, Proc. of the 7th  International Joint Conference on Theory and Practice of Software Development </i>, LNCS 1224, 1997.<P>
    15 
    16   <li> A proof of the Alternating Bit Protocol (ABP subdirectory) with unbounded buffers using 
    17        a combination of Isabelle and a model checker. This case study is performed within the 
    18        theory of IOA described above. For details see:<BR>
    19 Olaf M&uuml;ller and Tobias Nipkow,
    20 <A HREF="http://www4.informatik.tu-muenchen.de/papers/MuellerNipkow_TaAf1995.html">Combining Model Checking and Deduction for I/O Automata  </A>.
    21 In <i> TACAS'95, Proc. of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems </i>, LNCS 1019, 1995.<P>
    22    <li> A proof of a Network Transmission Protocol (NTP subdirectory) using the theory of IOA described above. For details see:<BR>
    23 
    24         Tobias Nipkow, Konrad Slind.
    25 <A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ioa.html>
    26 I/O Automata in Isabelle/HOL</A>. In <i>Types for Proofs and Programs</i>,
    27 LNCS 996, 1995, 101-119.
    28 
    29 </UL>
    30 
    31 </BODY></HTML>
    32 
    33 
    34