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