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.12 Sekunden
(vorverarbeitet am 2026-04-26)
¤
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.
