About FSA
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, Stark and Storm. 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…
IPA best PhD thesis award
Jan Martens received the IPA 2024 best PhD thesis award (click on the title for a link to the thesis).
Internships at CERN
CERN in Geneva is offering interesting internships.
Two STARK Contributions Accepted at Runtime Verification 2026
The paper ‘Monitoring under uncertainty with DisTL‘ by Sebastián Betancourt, Valentina Castiglioni, and Simone Tini has been accepted for the Runtime Verification 2026 (RV 2026) conference, which will take place in Kingston, Canada, from October …continue reading
Canonicity and Minimality for Simulation Equivalences at CONCUR’26
The paper ‘Minimal and Canonical Quotients for Simulation Equivalences’ by Eduardo Costa Martins and Tim Willemse was accepted at CONCUR’26. The paper deals with the problem of quotienting transition systems modulo coupled simulation equivalence and …continue reading
Vacancy for an Assistant Professor in FSA
We have an Assistant Professor vacancy in our group on the topic of Formal Methods and Neuro-Symbolic AI. The offered position is part of a broader department-wide mission-driven research collaboration on Zero-touch systems at the …continue reading
More news…
Events
- Colloquium 8 October 12.45 - 13.30, 2026, MF 6.132. Thomas Neele: A logical view on paradises in parity games, with some SMT help.
- Colloquium 1 October 12.45 - 13.30, 2026, MF 6.132. Valentina Castiglioni: Return to the origins: equivalences, approximations and metrics for nondeterministic probabilistic processes.
- Colloquium 24 September 12.45 - 13.30, 2026, MF 6.132. Sebastián Betancourt: Monitoring under uncertainty with DisTL.
- Colloquium 17 September 12.45 - 13.30, 2026, MF 6.132. Tom Verhoeff: The Picture-Hanging Puzzles: Recent Progress.
- Colloquium 10 September 12.45 - 13.30, 2026, MF 6.132. Arend Rensink: Visualising CTL Witnesses and Counterexamples.
- Colloquium 25 June 12.45 - 13.30, 2026, MF 6.132. Mara Miulescu: Efficient counterexamples in mCRL2.
- Colloquium 11 June 12.45 - 13.30, 2026, MF 6.132. Herman Geuvers: Positive Hennessy–Milner logic for directed branching bisimulation.

