Quick tool primer (showing creating sigs, relations, facts, running, showing the visualizer, showing changing styles in the visualizer, showing the generation of a counterexample)
Workshop
First steps (to learn: facts, running, checking)
Address book (to learn: mutation, translating invariants to preconditions)
The visualizer (to learn: attributes vs arcs, coloring, hiding, functions for additional decorations)
Concurrency (to learn: program counters, setup + steps, frame conditions, the types of conditions to write in run vs check)
Preparatory talk
Workshop
runvscheck)Things to cover