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 15composition. 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 34HREF="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> 43