src/HOL/UNITY/Simple/README.html
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 11195 65ede8dfe304
child 15283 f21466450330
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
     1 <!-- $Id$ -->
     2 <HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
     3 
     4 <H2>UNITY: Examples Involving Single Programs</H2>
     5 
     6 <P> The directory presents verification examples that do not involve program
     7 composition.  They are mostly taken from Misra's 1994 papers on ``New UNITY'':
     8 <UL>
     9 <LI>common meeting time (<A HREF="Common.thy"><CODE>Common.thy</CODE></A>)
    10 
    11 <LI>the token ring (<A HREF="Token.thy"><CODE>Token.thy</CODE></A>)
    12 
    13 <LI>the communication network
    14 (<A HREF="Network.thy"><CODE>Network.thy</CODE></A>)
    15 
    16 <LI>the lift controller (a standard benchmark) (<A HREF="Lift.thy"><CODE>Lift.thy</CODE></A>)
    17 
    18 <LI>a mutual exclusion algorithm (<A HREF="Mutex.thy"><CODE>Mutex.thy</CODE></A>)
    19 
    20 <LI><EM>n</EM>-process deadlock
    21 (<A HREF="Deadlock.thy"><CODE>Deadlock.thy</CODE></A>)
    22 
    23 <LI>unordered channel (<A HREF="Channel.thy"><CODE>Channel.thy</CODE></A>)
    24 
    25 <LI>reachability in directed graphs (section 6.4 of the book) (<A
    26 HREF="Reach.thy"><CODE>Reach.thy</CODE></A> and
    27 <A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>)
    28 </UL>
    29 
    30 <HR>
    31 <P>Last modified on $Date$
    32 
    33 <ADDRESS>
    34 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
    35 </ADDRESS>
    36 </BODY></HTML>