Research We investigate and develop theories, techniques and tools for modelling and analysing the behaviours of (concurrent) systems. Research focusses on process algebra, semantics, model checking, logics and satisfiability solving. Application areas include protocols, hardware designs, industrial control systems. Tools developed by the group include mCRL2 and MaDL. Read More…
Education We offer courses in Logic, Formal Methods, Model Checking and Automated Reasoning. We are always looking for enthusiastic people who are interested in a research project or thesis in our Master programme. Read More…
Our department has 25 (assistant) professor vacancies; some such positions may end up in our group. We encourage those with a Formal Methods background (broadly construed) to apply for a position (ASAP). For details, see …continue reading
New book: ‘Spelen met oneindigheid’
Hans Zantema has published a book (‘Spelen met oneindigheid, verrassende figuren en patronen’, in Dutch—English translation is work in progress) about infinite sequences and their visualisations, see this link. An interview with Hans can be …continue reading
Visitor: Maurice ter Beek
Maurice ter Beek (ISTI, CNR, Pisa) will be visiting us from 1-6 March. He’ll be working on variability parity games, together with Erik de Vink and Tim Willemse.
New book on mCRL2
The book ‘Understanding behaviour of distributed systems using mCRL2‘, written by Muhammad Atif and Jan Friso Groote has appeared in the Systems, Decision and Control series of Springer. It gives an introduction into mCRL2 with …continue reading
Journal paper on decomposing monolithic processes accepted for JLAMP
The journal article “Decomposing monolithic processes in a process algebra with multi-actions” by Maurice Laveaux and Tim A.C. Willemse has been accepted for publication at JLAMP as part of a special issue of ICE. The …continue reading
- Colloquium 23 March 12.45 - 13.30, 2023, MF 6.132. Flip van Spaendonck: Verification of the busy-forbidden protocol using an extension of the cones and foci proof framework.
- Colloquium 9 March 12.45 - 13.30, 2023, MF 6.132. Hans Zantema: Turtle figures of morphic sequences.
- Colloquium 23 February 12.45 - 13.30, 2023, MF 6.132. Thomas Neele: Operations on Fixpoint Equation Systems, a formalisation in Coq..
- Colloquium 16 February 12.45 - 13.30, 2023, MF 6.132. Kevin Jilissen: Restricting SysML Activity Diagrams to facilitate formal analysis.
- Colloquium 9 February 12.45 - 13.30, 2023, MF 6.132. Rick Erkens: Optimizing Term Rewriting with Creeper Trace Transducers.
- Colloquium 2 February 12.45 - 13.30, 2023, MF 6.132. Herman Geuvers: Apartness and Hennessy-Milner logic.