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…
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
Open PhD Position
The formal system analysis group has an open PhD position. Please contact us, in case you consider to strive towards a PhD and have strong background in mathematics and computer science. PhD on Uncertainty in …continue reading
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
Paper accepted at QEST+FORMATS 2026
The paper “Verification of parametric Markov Automata under time-bounded reachability” by Kevin van de Glind, Matthias Volk and Tim Willemse has been accepted for publication at QEST+FORMATS 2026. The paper introduces parametric Markov automata (pMA) …continue reading
Dutch Formal Methods Day @ TU/e
Big turn out at the Dutch Formal Methods Day at the TU/e today, co-organised by our own Jore Booy. And a great set of speakers!
More news…
Events
- 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.
- MSc Defence 8 June 15.00 - 16.00, 2026, MF 6.132. Wietske de Bondt: Modelling a Mechanical Lung Ventilator in Stark.
- MSc Defence 4 June 10.00 - 12.00, 2026, Atlas 0.710. Veerle Fürst: Decision Importance in Binary Decision Diagrams.
- Colloquium 28 May 12.45 - 13.30, 2026, MF 6.132. Myrthe Spronck: From full-read to instant-read models.
- Colloquium 21 May 12.45 - 13.30, 2026, MF 6.132. Kevin van de Glind: Verification of time-bounded reachability properties on parametric Markov Automata.
- Colloquium 7 May 12.45 - 13.30, 2026, MF 6.132. Sebastián Betancourt: Monitoring, STARK’s DisTL and its real-valued semantics.