This website is last updated on: 28-04-2017.

Modeling and analysis of communicating systems (book)

mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols. It can be run on Windows, Linux, Apple Mac OS X and FreeBSD.

The toolset supports a collection of tools for linearisation, simulation, state-space exploration and generation and tools to optimise and analyse specifications. Moreover, state spaces can be manipulated, visualised and analysed.

The mCRL2 toolset is developed at the department of Mathematics and Computer Science of the Technische Universiteit Eindhoven, in collaboration with CWI and the University of Twente.


mCRL2 received a prize for the distinguished user-assistance tool feature in the VerifyThis verification challenge held at ETAPS2015, in London. mCRL2 combined a rich specification language with excellent automatic reasoning features that made it an excellent tool to obtain insight in complex data structures and behaviours.


mCRL2 now can be compiled using Zapcc 1.0.1, a fast C++ compiler based on clang-5.0. This speeds up the compilation with about 40%. To make it work add */libraries/utilities/source/command_line_interface.cpp to the [DoNotZap] section in bin/zapccs.config.

Next topic

mCRL2 user documentation