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
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!
Mohammad Reza Mousavi visits FSA
We have the pleasure of Mohammad Mousavi (King’s College, UK), former professor in the FSA group, visiting our group on the occasion of Tom Franken’s defence. Mohammad will give a talk about testing for quantum …continue reading
FSA at CAV’26
The paper “Scalable Deductive Verification of Data-Level Parallel Programs” by Lars B. van den Haak, Marieke Huisman and Anton Wijs has been accepted for publication at CAV 2026. This paper introduces several techniques that improve …continue reading
More news…
Events
- 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.
- Colloquium 30 April 12.45 - 13.30, 2026, MF 6.132. Eduardo Costa Martins: The Complexity of Quotienting Simulation Equivalences.