Publications
Note
If you refer to mCRL2 in your academic paper, we would appreciate it if you use the following references:
General
J.F. Groote, J.J.A. Keiren, B. Luttik, E.P. de Vink, T.A.C. Willemse. Modelling and Analysing Software in mCRL2. FACS 2019, LNCS vol. 12018, pp. 25-48. (DOI)
O. Bunte, J.F. Groote, J.J.A. Keiren, M. Laveaux, T. Neele, E.P. de Vink, J.W. Wesselink, A.J. Wijs, T.A.C. Willemse. The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability. TACAS 2019, LNCS vol. 11428, pp. 21-39. (DOI)
J.F. Groote, M.R. Mousavi. Modeling and analysis of communicating systems. The MIT press. 2014.
S. Cranen, J.F. Groote, J.J.A. Keiren, F.P.M. Stappers, E.P. de Vink, J. W. Wesselink, T.A.C. Willemse. An Overview of the mCRL2 Toolset and Its Recent Advances. TACAS 2013, pages 199-213. (DOI)
J.F. Groote, J.J.A. Keiren, F.P.M. Stappers, J.W. Wesselink and T.A.C. Willemse. Experiences in developing the mCRL2 toolset. In Software: Practice and Experience, 41(2): 143-153, 2011. (DOI)
J.F. Groote, A. Mathijssen, M.A. Reniers, Y.S. Usenko, M.J. van Weerdenburg. Analysis of distributed systems with mCRL2. In M. Alexander, W. Gardner (Eds.), Process Algebra for Parallel and Distributed Processing, pages 99-128. Chapman and Hall, 2008
J.F. Groote, J.J.A. Keiren, A. Mathijssen, B. Ploeger, F.P.M. Stappers, C. Tankink, Y.S. Usenko, M.J. van Weerdenburg, J.W. Wesselink, T.A.C. Willemse and J. van der Wulp. The mCRL2 toolset. In: Proc. International Workshop on Advanced Software Development Tools and Techniques (WASDeTT 2008), 2008. (http://scg.unibe.ch/download/wasdett/wasdett2008-paper05.pdf).
J.F. Groote, A. Mathijssen, M.A. Reniers, Y.S. Usenko, M.J. van Weerdenburg. The Formal Specification Language mCRL2. In: Proc. Methods for Modelling Software Systems. Dagstuhl Seminar Proceedings 06351, 2007. (http://drops.dagstuhl.de/opus/volltexte/2007/862/pdf/06351.GrooteJanFriso.Paper.862.pdf).
J.F. Groote, A. Mathijssen, M.J. van Weerdenburg, Y.S. Usenko. From µCRL to mCRL2: Motivation and Outline. In: Proc. Workshop Essays on Algebraic Process Calculi (APC 25). ENTCS 162 (2006), pp 191-196. Also appeared in the BRICS Notes Series. (DOI)
J.F. Groote and M.A. Reniers. Algebraic process verification. In J. A. Bergstra, A. Ponse and S. A. Smolka. Handbook of Process Algebra, pages 1151-1208, Elsevier, Amsterdam, 2001. Also appeared as a technical report. (DOI)
Research
A. Stramaglia, J.J.A. Keiren, T. Neele. Simplifying Process Parameters by Unfolding Algebraic Data Types. ICTAC 2023. LNCS vol. 14446, pp. 399-416. (DOI)
J.J.M. Martens and J.F. Groote. Computing Minimal Distinguishing Hennessy-Milner Formulas is NP-Hard, but Variants are Tractable. CONCUR 2023, LIPIcs vol. 279. (DOI)
D.N. Jansen, J.F. Groote, J.J.A. Keiren, A. Wijs. An O(m log n) algorithm for branching bisimilarity on labelled transition systems. TACAS 2020, LNCS vol. 12079, pp. 3-20. (DOI)
T. Neele, W. Wesselink, T.A.C. Willemse. Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems. TACAS 2020, LNCS vol. 12079, pp. 307-324. (DOI)
T. Neele, T.A.C. Willemse and J.F. Groote. Finding compact proofs for infinite-data parameterised Boolean equation systems. Science of Computer Programming (FACS 2018 special issue), vol. 188, pp. 102389. (DOI)
M. Laveaux, J.F. Groote, T.A.C. Willemse. Correct and Efficient Antichain Algorithms for Refinement Checking. FORTE 2019, LNCS vol. 11535, pp. 185-203. (DOI)
T. Neele, T.A.C. Willemse and J.F. Groote. Solving Parameterised Boolean Equation Systems with Infinite Data Through Quotienting. In FACS 2018. LNCS, vol. 11222, pp. 216–236. (DOI)
J.W. Wesselink and T.A.C. Willemse. Evidence Extraction from Parameterised Boolean Equation Systems. In ARQNL 2018, CEUR workshop proceedings, vol. 2095, pp. 86–100. (link)
S. Cranen, J.J.A. Keiren, and T.A.C. Willemse. Parity game reductions. Acta Informatica 55(5): 401-444, 2018. (DOI)
R.P.J. Koolen, T.A.C. Willemse, and H. Zantema. Using SMT for Solving Fragments of Parameterised Boolean Equation Systems. In ATVA 2015, LNCS vol. 9364, pp. 14–30. (DOI)
J.J.A. Keiren, J.W. Wesselink, and T.A.C. Willemse. Liveness Analysis for Parameterised Boolean Equation Systems. In F. Cassez, J.F. Raskin (eds), Automated Technology for Verification and Analysis. ATVA 2014. Lecture Notes in Computer Science, vol 8837. Springer, Cham, pp. 219–234, 2014. See also this arXiv preprint. 2014. (DOI)
J.J.A. Keiren, M.A. Reniers and T.A.C. Willemse. Structural Analysis of Boolean Equation Systems. In ACM Transactions on Computational Logic 13(1): 8-1/35, 2012. (DOI)
M. Gazda and T.A.C. Willemse. Consistent Consequence for Boolean Equation Systems. In M. Bielikova et al. (eds), 38th International Conference on Current Trends in Theory and Practice of Computer Science, SOFSEM 2012, Lecture Notes in Computer Science 7147, Springer, pp. 277–288, 2012. (DOI)
S. Cranen, J.J.A. Keiren and T.A.C. Willemse, A Cure for Stuttering Parity Games. In A. Roychoudhury, M. D’Souza (eds.), Theoretical Aspects of Computing - 9th International Colloqium, ICTAC 2012, Lecture Notes in Computer Science 7521, Springer-Verlag, pp.198-212, 2012. The full version containing detailed proofs is available as a technical report. 2012. (DOI)
S. Cranen, J.J.A. Keiren and T.A.C. Willemse. Stuttering Mostly Speeds Up Solving Parity Games. In M. Gheorghiu Bobaru, K. Havelund, G.J. Holzmann, R. Joshi (eds.), NASA Formal Methods - Third International Symposium, NFM 2011, Lecture Notes in Computer Science 6617, Springer-Verlag, pp. 207-221, 2011. See also this arXiv preprint. 2011. (DOI)
B. Ploeger, J.W. Wesselink and T.A.C. Willemse. Verification of Reactive Systems via Instantiation of Parameterised Boolean Equation Systems. In Information and Computation, 209(4):637-663. 2011. An extended abstract appeared in ICTAC 2008, see also the technical report. (DOI)
J.J.A. Keiren and T.A.C. Willemse. Bisimulation Minimisations for Boolean Equation Systems. In K. Namjoshi, A. Zeller & A. Ziv (Eds.), Hardware and Software: Verification and Testing (5th International Haifa Verification Conference, HVC 2009. Lecture Notes in Computer Science, Vol. 6405, pp. 102-116. Springer. 2011. (DOI)
J.J.A. Keiren, M.A. Reniers. Type checking mCRL2. Computer Science Report No. 11-11, Eindhoven: Technische Universiteit Eindhoven, 21 pp. 2011. (http://alexandria.tue.nl/repository/books/716663.pdf).
T.A.C. Willemse. Consistent Correlations for Parameterised Boolean Equation Systems with Applications in Correctness Proofs for Manipulations. In P. Gastin and F. Laroussinie (eds.), Concurrency Theory, 21st International Conference, CONCUR 2010, Paris, France, Lecture Notes in Computer Science 6269, Springer-Verlag, pp. 584–598, 2010. (DOI)
S.M. Orzan and T.A.C. Willemse. Invariants for Parameterised Boolean Equation Systems. In Theoretical Computer Science, 411(11-13):1338-1371, 2010. An extended abstract occurred in CONCUR 2008, see also the technical report. (DOI)
T.A.N. Engels, J.F. Groote, M.J. van Weerdenburg and T.A.C. Willemse. Search Algorithms for Automated Validation. Journal of Logic and Algebraic Programming, volume 78, issue 4, pages 274-287, 2009. Also appeared as a technical report. (DOI)
S.M. Orzan, J.W. Wesselink and T.A.C. Willemse. Static Analysis Techniques for Parameterised Boolean Equation Systems. In S. Kowalewski and A. Philippou (eds.), TACAS 2009, Lecture Notes in Computer Science 5505, pp. 230–245, 2009. (DOI)
B. Ploeger and C. Tankink. Improving an Interactive Visualization of Transition Systems. In: Proceedings of the 4th ACM Symposium on Software Visualization 2008 (SoftVis 2008), pages 115-124. ACM, 2008. (DOI)
R.J. van Glabbeek and B. Ploeger. Correcting a Space-Efficient Simulation Algorithm. In: Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), LNCS 5123, pages 517-529. Springer, 2008. Also available as technical report. (DOI)
M. van Weerdenburg, Process Algebra with Local Communication, Proceedings of the 4th International Workshop on Formal Aspects of Component Software (FACS 2007), volume 215 of Electronic Notes in Theoretical Computer Science, pp. 191-208, 2008. Also appeared as a technical report. (DOI)
T. Chen, B. Ploeger, J. van de Pol and T.A.C. Willemse. Equivalence Checking for Infinite Systems using Parameterized Boolean Equation Systems. In: Proceedings of the 18th International Conference on Concurrency Theory (CONCUR 2007), LNCS 4703, pages 120-135. Springer, 2007. Also available as technical teport. (DOI)
M. van Weerdenburg, An Account of Implementing Applicative Term Rewriting, Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2006), volume 174/10 of Electronic Notes in Theoretical Computer Science, pp. 139-155, 2007. Also appeared as a technical report. (DOI)
J.F. Groote and F.J.J. van Ham. Interactive visualization of large state spaces. International Journal on Software Tools for Technology Transfer 8:77-91, 2006. An early version appeared as a technical report. (DOI)
J.F. Groote and T.A.C. Willemse. Parameterised Boolean Equation Systems. In Theoretical Computer Science, 343:332-369, 2005. Also appeared as a technical report and an extended abstract at CONCUR 2004. (DOI)
J.F. Groote and M. Keinänen. A Sub-quadratic Algorithm for Conjunctive and Disjunctive Boolean Equation Systems. In D.V. Hung and M. Wirsing, editors, Proceedings of International Colloquium on Theoretical Aspects of Computing (ICTAC’2005), LNCS 3722, pages 545-558. Springer-Verlag, 2005. Also appeared as a technical report. (DOI)
J.F. Groote and T.A.C. Willemse. Model-checking processes with data. Science of Computer Programming, 56:251-273, 2005. Also appeared as a technical report and a short version at FMCO 2003. (DOI)
J.F. Groote and M.K. Keinänen. Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points. In K. Jensen and A. Podelski, editors, Proc. 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’2004), LNCS 2988, pages 436-450. Springer, 2004. Also appeared as a technical report. (DOI)
Applications
T. Neele, M. H. Rol, J. F. Groote. Verifying System-Wide Properties of Industrial Component-Based Software. In FSEN 2019, LNCS vol. 11761, pp. 158-175. (DOI)
R. van Beusekom, J. F. Groote, P. Hoogendijk, R. Howe, J. W. Wesselink, R. Wieringa, and T. A. C. Willemse. Formalising the Dezyne Modelling Language in mCRL2. In FMICS-AVoCS 2017, LNCS vol. 10471, pp. 217-233. (DOI)
Daniela Remenska, Jeff Templon, Tim A.C. Willemse, Philip Homburg, Kees Verstoep , Adria Casajus and Henri Bal. From UML to Process Algebra and Back: An Automated Approach to Model-Checking Software Design Artifacts of Concurrent Systems. In Guillaume Brat, Neha Rungta, Arnaud Venet (eds.), NFM 2013, Lecture Notes in Computer Science 7871, Springer, pp. 244-260, 2013. (DOI)
Y.L. Hwong, J.J.A. Keiren, V.J.J. Kusters, S. Leemans, T.A.C. Willemse. Formalising and Analysing the Control Software of the Compact Muon Solenoid Experiment at the Large Hadron Collider. Accepted for publication in Science of Computer Programming. 2013. An extended abstract appeared at FSEN 2011 and as CoRR abs/1101.5324. See also Control Software of the CMS Experiment at CERN’s Large Hadron Collider and (DOI)
D. Remenska, T.A.C. Willemse, K. Verstoep, W. Fokkink, J. Templon, H. Bal, Using Model Checking to Analyze the System Behavior of the LHC Production Grid. In 12th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing, CCGrid 2012, pp. 335-343, 2012. (DOI)
S. Cranen. Model checking the FlexRay start-up phase. In M. Stoelinga & R. Pinger (Eds.), Formal Methods for Industrial Critical Systems - 17th International Workshop, FMICS 2012, LNCS 7437, Springer, pp. 131-145). Also appeared as a technical report. (DOI)
J.J.A. Keiren, M.D. Klabbers. Modelling and verifying IEEE Std 11073-20601 session setup using mCRL2. Proc. 12th International Workshop on Automated Verification of Critical Systems (AVoCS 2012). In G. Luettgen, S. Merz (eds.), Electroning Communications of the EASST, 2012. (DOI)
Stappers, F.P.M., Reniers, M.A., Groote, J.F., Weber, S., Dogfooding the structural operational semantics of mCRL2, Computer Science Report, No. 11-18, Eindhoven: Technische Universiteit Eindhoven, 87 pp, 2011 (see also Dogfooding the structural operational semantics of mCRL2 and http://alexandria.tue.nl/repository/books/724474.pdf).
B. Ploeger. Analysis of ACS using mCRL2. CS-Report 09-11, Technische Universiteit Eindhoven, 2009 (see also Atacama Large Millimeter Array and http://alexandria.tue.nl/repository/books/653251.pdf).
F.P.M. Stappers and M.A. Reniers. “Verification of safety requirements for program code using data abstraction”. Proc. Ninth International Workshop on Automated Verification of Critical Systems (AVoCS 2009), pages 3-25, 2009. See also PCB Printer and (DOI)
W.J. Fokkink, P. Klint, B. Lisser, Y.S. Usenko, Towards formal verification of ToolBus scripts, In J. Meseguer and G. Rosu, eds., Proc. AMAST’08, 28-31 July, 2008, Urbana-Champaign, IL, USA, LNCS 5140, Springer. (DOI)
H. Hojjat, M.R. Mousavi, M. Sirjani, Process Algebraic Verification of SystemC Codes, Proceedings of the 8th International Conference on Application of Concurrency to System Design (ACSD’08), Xi’an, China, IEEE CS, June 2008. Also appeared as a technical report. (DOI)
K.L. Man, J. van der Wulp, Specification and Analysis of Hardware Designs using mCRL2, IEEE Proceedings of the 21st IEEE Canadian Conference on Electrical and Computer Engineering, Niagara Falls, Canada, May 2008. (DOI)
J.F. Groote, M.A. Reniers, Y.S. Usenko, Verification of Networks of Timed Automata using mCRL2, 16th Int. Workshop on Parallel and Distributed Real-Time Systems (WPDRTS’08), April 14, 2008, Miami, Florida, USA. (DOI)
Algebraic Software Analysis and Embedded Simulation of a Driving Robot. Leon Merkx, Hans-Martin Duringhof, Pieter Cuijpers. 2007 Summer Computer Simulation Conference (SCSC) in San Diego, CA. Also appeared as technical report. See also Generic Driving Actuator and (DOI)
J.E. Wiggelinkhuizen. Feasibility of formal model checking in the Vitatron environment. Master Thesis. Eindhoven University of Technology, 2007 (see also Pacemaker and http://alexandria.tue.nl/extra2/afstversl/wsk-i/wiggelinkhuizen2007.pdf).
H. Hojjat, M. Sirjani, M.R. Mousavi, J.F. Groote, Sarir: A Rebeca to mCRL2 Translator (Tool Paper). Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD’07), Bratislava, Slovak Republic, IEEE CS, July 2007. (DOI)
M. van Eekelen, S. ten Hoedt, R. Schreurs, Y.S. Usenko, Analysis of a Session-Layer Protocol in mCRL2. Verification of a Real-Life Industrial Implementation. Proc. 12th FMICS 2007. 1-2 July 2007. Berlin. LNCS 4916. Also appeared as technical report. See also AIA ITP load-balancer and (DOI)
I. Raedts, M. Petkovic, Y.S. Usenko, J.M. van der Werf, J.F. Groote, L.J. Somers, Transformation of BPMN models for behaviour analysis, In J.C. Augusto, J. Barjis, U. Ultes-Nitsche, eds., Proc. 5th MSVVEIS’07, pp. 126–137, Funchal, Madeira, Portugal, June 2007.
A. Mathijssen, A.J. Pretorius. Verified Design of an Automated Parking Garage. Proc. FMICS and PDMC 2006. LNCS 4346 (2007), pages 165-180. Also appeared as technical report. See also Automated parking garage, and (DOI)
B. Ploeger and L. Somers. Analysis and Verification of an Automatic Document Feeder. In: “Proceedings of the 2007 ACM Symposium on Applied Computing (ACMSAC’07)”, pages 1499-1505, Seoul, Korea. ACM, March 2007. Also appeared as a technical report. See also Automatic Document Feeder, and (DOI)
B. Badban, W. Fokkink, J.F. Groote, J. Pang and J.C. van de Pol. Verification of a sliding window protocol in μCRL and PVS. Formal Aspects of Computing 17(3):342-388, 2005. Also appeared as a technical report. (DOI)
Analysis of a distributed system for lifting trucks. J.F. Groote, J. Pang, and A. Wouters. Journal of Logic and Algebraic Programming, 55(1-2): 21-56, 2003. See also Distributed system for lifting trucks and (DOI)
Description and formal specification of the Link Layer of P1394. S. P. Luttik. In: Ignac Lovrek, editor, Proceedings of the 2nd International Workshop on Applied Formal Methods in System Design, University of Zagreb, Croatia. Also appeared as technical report. See also IEEE 1394 link layer.
Course material
- [GM14]
J.F. Groote, M.R. Mousavi. Modeling and analysis of communicating systems. The MIT press. 2014.
- [GMPR06]
J.F. Groote, A. Mathijssen, B. Ploeger, M.A. Reniers, M.J. van Weerdenburg, J. van der Wulp. Process Algebra and mCRL2 , IPA Basic Course on Formal Methods 2006.
Presentations
A. Mathijssen. Analysis of system behaviour using the mCRL2 toolset. Bits&Chips 2008 Embedded Systemen, Evoluon Eindhoven, 9th October, 2008.
A. Mathijssen, B. Ploeger, F.P.M. Stappers, T.A.C. Willemse. Behaviour Analysis using mCRL2. IPA Course on Formal Methods, Eindhoven University of Technology, 26th June 2008.