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 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…
Open PhD Positions
The formal system analysis group has several open PhD positions, targeting various topics that range from pure theory to applied formal methods. Please contact us, in case you consider to strive towards a PhD and …continue reading
An Expressive Timed Modal Mu-Calculus for Timed Automata @ QEST+FORMATS
The paper An expressive Timed Modal Mu-Calculus for Timed Automata by Rance Cleaveland, Jeroen Keiren and Peter Fontana, accepted for publication at QEST+FORMATS (Calgary, September 2024) is now available in LNCS vol. 14996.
Progress, Justness and Fairness in the modal mu-calculus @ CONCUR
The paper ‘Progress, Justness and Fairness in modal mu-calculus formulae’, by Myrthe Spronck, Bas Luttik and Tim Willemse , recently accepted for presentation at CONCUR (September 2024, Calgary, Canada) is now available, see LIPIcs, volume 311.
Paper accepted for CASE 2024
The paper Validation of Supervisory Control Synthesis Tool CIF Using Model Checker mCRL2 by Michel Reniers and Jeroen Keiren has been accepted for IEEE CASE 2024. The paper describes how the mCRL2 model checker can …continue reading
ABZ 2024 case study paper published
The paper Modelling and Analysing a Mechanical Lung Ventilator in mCRL2 by Danny van Dortmont, Jeroen Keiren and Tim Willemse has been published at ABZ 2024. The paper describes the modelling and analysis of the …continue reading
ACM TOCL paper published
The paper Extensible Proof Systems for Infinite-State Systems by Rance Cleaveland and Jeroen Keiren has appeared in ACM Transactions on Computational Logic. The paper revisits soundness and completeness of proof systems for proving that sets …continue reading
More news…
Events
- Colloquium 5 September 12.45 - 13.30, 2024, MF 6.132. Gwen Salaün: Automated Verification of Textual Process Descriptions.
- Colloquium 4 July 12.45 - 13.30, 2024, MF 6.132. Erik de Vink: On an Auxilliary Notion of Probabilistic Inclusion.
- Colloquium 27 June 12.45 - 13.30, 2024, MF 6.132. Hans Zantema: Morphic sequences: characterization, visualization and equality.
- Colloquium 20 June 12.45 - 13.30, 2024, MF 6.132. Jeroen Keiren: Validation of supervisory control synthesis tool CIF using model checker mCRL2.
- Colloquium 13 June 12.45 - 13.30, 2024, MF 6.132. Jeroen Keiren: It’s all a game: Bisimulation and Apartness.
- Colloquium 6 June 12.45 - 13.30, 2024, MF 6.132. Edward Liem: Towards Optimizing Feature Cause Computations.
- Colloquium 30 May 12.45 - 13.30, 2024, MF 6.132. Anton Wijs: Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking.