DLL.java demonstration using the http://lara.epfl.ch/w/jahob_system (Also: one can remove invariant that there is only one list, but must strengthen some preconditions.)

Need for expressing reachability in graphs

Weak Monadic Logic of One Successor

Using Automata to Decide WS1S

Continued in Exercise 13