Publications

From MCRL2

Contents 1 General 2 Research 3 Applications 4 Course material 5 Presentations

General

• Jan Friso Groote, Jeroen Keiren, Aad Mathijssen, Bas Ploeger, Frank Stappers, Carst Tankink, Yaroslav Usenko, Muck van Weerdenburg, Wieger Wesselink, Tim Willemse and Jeroen van der Wulp. The mCRL2 toolset . In: Proc. International Workshop on Advanced Software Development Tools and Techniques (WASDeTT 2008).
• Jan Friso Groote, Aad Mathijssen, Michel Reniers, Yaroslav Usenko, Muck van Weerdenburg. The Formal Specification Language mCRL2 . In: Proc. Methods for Modelling Software Systems. Dagstuhl Seminar Proceedings 06351 (2007).
• Jan Friso Groote, Aad Mathijssen, Muck van Weerdenburg, Yaroslav 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 .
• 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 .

Research

• Tom A.N. Engels, Jan Friso Groote, Muck J. van Weerdenburg and Tim A.C. Willemse. Search Algorithms for Automated Validation. Accepted for publication in the Journal of Logic and Algebraic Programming. Also appeared as a technical report .
• 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.
• A. van Dam, B. Ploeger and T.A.C. Willemse. Instantiation for Parameterised Boolean Equation Systems. In: Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing (ICTAC 2008), LNCS 5160, pages 440-454. Springer, 2008. Also available as technical report .
• S.M. Orzan and T.A.C. Willemse, Invariants for Parameterised Boolean Equation Systems (extended abstract). In F. van Breugel, M. Chechik, editors, Concurrency Theory, 19th International Conference, CONCUR 2008, Toronto, Canada, Lecture Notes in Computer Science 5201, Springer-Verlag, pp. 187--202, 2008. Also appeared as a technical report .
• 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 .
• 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 .
• 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 .
• 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 .
• 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 .
• 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.
• 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 .
• 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 .
• 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.

Applications

• 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.
• 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 .
• 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.
• 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.
• 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.
• 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 a technical report .
• 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.
• Aad Mathijssen, A. Johannes Pretorius. Verified Design of an Automated Parking Garage. Proc. FMICS and PDMC 2006. LNCS 4346 (2007), pages 165-180. Also appeared as technical report .
• 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 .

Course material

• Jan Friso Groote, Aad Mathijssen, Bas Ploeger, Michel Reniers, Muck van Weerdenburg, Jeroen van der Wulp. Process Algebra and mCRL2 , IPA Basic Course on Formal Methods 2006.

Presentations

• Aad Mathijssen. Analysis of system behaviour using the mCRL2 toolset . Bits&Chips 2008 Embedded Systemen, Evoluon Eindhoven, 9th October, 2008.
• Aad Mathijssen, Bas Ploeger, Frank Stappers, Tim Willemse. Behaviour Analysis using mCRL2 . IPA Course on Formal Methods, Eindhoven University of Technology, 26th June 2008.