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

Posted in People, Research | Comments Off on Open PhD Positions

Paper accepted for TCS

The following paper has been accepted for publication in Theoretical Computer Science: Robustness for biochemical networks: Step-by-step approach by Valentina Castiglioni, Ruggero Lanotte, Michele Loreti, Desiree Manicardi, and Simone Tini. The paper will be published …continue reading

Posted in Research | Comments Off on Paper accepted for TCS

RobTL: Robustness Temporal Logic for CPS @ CONCUR

The paper ‘RobTL: Robustness Temporal Logic for CPS’, by Valentina Castiglioni, Michele Loreti and Simone Tini , recently accepted for presentation at CONCUR (September 2024, Calgary, Canada) is now available, see LIPIcs, volume 311 [doi]

Posted in Research | Comments Off on RobTL: Robustness Temporal Logic for CPS @ CONCUR

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.

Posted in Research | Comments Off on An Expressive Timed Modal Mu-Calculus for Timed Automata @ QEST+FORMATS

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.

Posted in Research | Comments Off on Progress, Justness and Fairness in the modal mu-calculus @ CONCUR

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

Posted in Research | Comments Off on Paper accepted for CASE 2024

More news…