This website is last updated on: 22-03-2019.

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 the University of Twente.


On Coursera four consecutive courses consisting of approximately 60 lectures provide an introduction into the theory and practical use of the mCRL2 toolset. It is based on the book ‘Modeling and Analysis of Communicating Systems’ shown above. The courses are:

The slides used to make these courses are available by contacting They can also be downloaded from MIT Press.


Verum is the industry leader in reliable software design.

mCRL2 is used by the company Verum as their verification engine. Verum provides model based software development environments for the languages ASD and Dezyne that allow to program proven correct embedded software with much less effort than “classical” programming. As it stands Verum is the industry leader in reliable software design.


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.

TeamCity The mCRL2 project uses TeamCity for regression testing during development and building the daily snapshots.