Automated Exercise Generation for Satisfiability Checking
Graphical Loop Invariant Based Programming
A Gentle Introduction to Verification of Parameterized Reactive Systems
Model Checking Concurrent Programs for Autograding in pseuCo Book
Teaching TLA+ to Engineers at Microsoft
Teaching and Training in Formalisation with B
Teaching low-code Formal Methods with Coloured Petri Nets.