equal
deleted
inserted
replaced
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
|
2 |
|
3 <HTML> |
|
4 |
|
5 <HEAD> |
|
6 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> |
|
7 <TITLE>HOL/UNITY/README</TITLE> |
|
8 </HEAD> |
|
9 |
|
10 <BODY> |
|
11 |
|
12 <H2>UNITY: Examples Involving Single Programs</H2> |
|
13 |
|
14 <P> The directory presents verification examples that do not involve program |
|
15 composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'': |
|
16 <UL> |
|
17 <LI>common meeting time (<A HREF="Common.thy"><CODE>Common.thy</CODE></A>) |
|
18 |
|
19 <LI>the token ring (<A HREF="Token.thy"><CODE>Token.thy</CODE></A>) |
|
20 |
|
21 <LI>the communication network |
|
22 (<A HREF="Network.thy"><CODE>Network.thy</CODE></A>) |
|
23 |
|
24 <LI>the lift controller (a standard benchmark) (<A HREF="Lift.thy"><CODE>Lift.thy</CODE></A>) |
|
25 |
|
26 <LI>a mutual exclusion algorithm (<A HREF="Mutex.thy"><CODE>Mutex.thy</CODE></A>) |
|
27 |
|
28 <LI><EM>n</EM>-process deadlock |
|
29 (<A HREF="Deadlock.thy"><CODE>Deadlock.thy</CODE></A>) |
|
30 |
|
31 <LI>unordered channel (<A HREF="Channel.thy"><CODE>Channel.thy</CODE></A>) |
|
32 |
|
33 <LI>reachability in directed graphs (section 6.4 of the book) (<A |
|
34 HREF="Reach.thy"><CODE>Reach.thy</CODE></A> and |
|
35 <A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>) |
|
36 </UL> |
|
37 |
|
38 <ADDRESS> |
|
39 <A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
|
40 </ADDRESS> |
|
41 </BODY> |
|
42 </HTML> |
|