section‹UNITY: Examples Involving Single Programs›
text‹
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›> ›
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
