The directory presents verification examples that do not involve program composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'':
Common.thy
)
Token.thy
)
Network.thy
)
Lift.thy
)
Mutex.thy
)
Deadlock.thy
)
Channel.thy
)
Reach.thy
and
Reachability.thy
)