HOL/UNITY/README

diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/UNITY/Simple/README.html Mon Mar 05 15:47:11 2001 +0100 @@ -0,0 +1,36 @@ + +HOL/UNITY/README + +

UNITY: Examples Involving Single Programs

+ +

The directory presents verification examples that do not involve program +composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'': +

common meeting time (Common.thy) + +
the token ring (Token.thy) + +
the communication network +(Network.thy) + +
the lift controller (a standard benchmark) (Lift.thy) + +
a mutual exclusion algorithm (Mutex.thy) + +
n-process deadlock +(Deadlock.thy) + +
unordered channel (Channel.thy) + +
reachability in directed graphs (section 6.4 of the book) (Reach.thy and +Reachability.thy) +

+ +

Last modified on $Date$ + +

+lcp@cl.cam.ac.uk +