Modelling and analysing software in mCRL2

Research output: Book/ReportReportAcademic

23 Downloads (Pure)


Model checking is an effective way to design correct software.
Making behavioural 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.
Original languageEnglish
Place of PublicationEindhoven
PublisherTechnische Universiteit Eindhoven
Number of pages24
Publication statusPublished - Dec 2019

Publication series

NameComputer Science Reports
ISSN (Print)0926-4515


Cite this

Groote, J. F., Keiren, J. J. A., Luttik, B., de Vink, E. P., & Willemse, T. A. C. (2019). Modelling and analysing software in mCRL2. (Computer Science Reports; Vol. 19-05). Eindhoven: Technische Universiteit Eindhoven.