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)