Teaching Concurrency with the Disappearing Formal Method

The Gries-Owicki non-interference condition is fundamental to concurrent programming, but difficult to explain as it relies on proof outlines rather than only pre- and postconditions. This paper reports on teaching a practical course on concurrent programming using hierarchical state diagrams to visualize concurrent programs and argue for their correctness, including non-interference.