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›> ›
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet am 2026-06-30)
¤
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.
