Quelle  README_Simple.thy   Sprache: Isabelle

theory README_Simple imports Main
begin

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