The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in
Expressivity and Usability

Jan Friso Groote, Jeroen J.A. Keiren, Bas Luttik, Erik P. de Vink, 
and Tim A.C. Willemse

Model checking is an effective way to design correct software. Making
behavioral models of software, formulating correctness properties using modal
formulas, and verifying these using finite state analysis techniques, is a very
efficient way to obtain the required insight in the software. We illustrate
this on four common but tricky examples.