Theory README_Simple

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