Projects per year
Organisation profile
Introduction / mission
Formal System Analysis focuses on theories, techniques and tools for modeling and analyzing the behaviors of software-controlled systems.
Highlighted phrase
Investigating and developing theories, techniques and tools for modelling and analysing the behaviours of (concurrent) systems.
Organisation profile
The FSA group studies the foundations of software-controlled systems and develops languages and techniques for modelling and analyzing real-world, industrial-scale applications. Expertise in the group includes process algebras for reasoning about concurrent, timed and probabilistic system behavior, SAT- and SMT-solvers, rewriting, and model checking technology. Research focusses on scalability of the technology, which is required for its use in the development of software controlled-systems. The group offers master courses in LogicComputer checked theorem proving, Formal MethodsSoftware Modelling and Analysis, Process Algebras, Model Checking, Micro-processor Verification, and Automated Reasoning. Much of the group’s research is consolidated in tools. The most prominent examplesinclude is mCRL2. mCRL2 is a process-algebraic language with an award-winning tool set for modeling and analyzing concurrent systems.
Current areas of application include protocols, hardware designs and industrial control systems. Recent examples include the formalization of the commercial industrial modelling and code generation language Dezyne, which relies on mCRL2 for analyzing the system behaviors. Past examples include verification of the control systems of the four large experiments in the Large Hadron Collider at CERN, using model checking and satisfiability solving to improve the control system reliability, and the analysis of the software architecture of the first award-winning Stella Solar Car.
Recent research projects in which FSA is involved include:
• AVVA: Accelerated Verification and Verification Accelerated (NWO TOP grant)
• MERITS: Model extraction for re-engineering traditional software (NWO Big Software, with Philips Healthcare)
• Formal verification of cache coherent multi-core architectures (NWO TOP grant)
Formal modelling and analysis is essential for cost-effective design of highly reliable software-controlled systems.
UN Sustainable Development Goals
In 2015, UN member states agreed to 17 global Sustainable Development Goals (SDGs) to end poverty, protect the planet and ensure prosperity for all. Our work contributes towards the following SDG(s):
-
SDG 7 Affordable and Clean Energy -
SDG 14 Life Below Water
Fingerprint
Dive into the research topics where Formal System Analysis is active. These topic labels come from the works of this organisation's members. Together they form a unique fingerprint.
Collaborations and top research areas from the last five years
Recent external collaboration on country/territory level. Dive into details by clicking on the dots or
Profiles
-
Menno Bartels
- Mathematics and Computer Science, Algorithms and Logics for Verification - Doctoral Candidate-TA
Person: OWP : University Teacher / Researcher
-
Roel Bloo
- Mathematics and Computer Science, Algorithms and Logics for Verification - University Lecturer
- Mathematics and Computer Science, Formal System Analysis - University Lecturer
Person: OWP : University Teacher / Researcher
Projects
- 2 Finished
-
11181-A1504 ES Education at TU/e
de With, P. H. N. (Project member), Lukkien, J. J. (Project member), Klabbers, M. D. (Project member), Cuijpers, P. J. L. (Project member), Reymen, I. M. M. J. (Project member), Basten, A. A. (Project member), Groote, J. F. (Project member), Luttik, S. P. (Project Manager), Luttik, S. P. (Project member), van den Brand, M. G. J. (Project member), Özçelebi, T. (Project member), Nabi, M. (Project member), Dubbelman, G. (Project member) & Adriaans-Van der Palen, I. (Project member)
1/01/15 → 31/12/15
Project: Research direct
-
Composable Embedded Systems for Healthcare
Groote, J. F. (Project Manager) & Vlasiou, M. (Project member)
1/05/11 → 30/06/17
Project: Research direct
-
A Method for Testing Partial-Order Reduction Theories in Alloy
Miulescu, M. (Corresponding author) & Neele, T., 22 May 2026, Rigorous State-Based Methods: 12th International Conference, ABZ 2026, Tokyo, Japan, May 18–20, 2026, Proceedings. Ishikawa, F. & Cunha, A. (eds.). Cham: Springer, p. 126-144 19 p. (Lecture Notes in Computer Science (LNCS); vol. 16579).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
-
A Parallel Programming Perspective: Designing AuDaLa and AuDaLogic
Franken, T. T. P., 3 Jun 2026, Eindhoven: Eindhoven University of Technology. 364 p.Research output: Thesis › Phd Thesis 1 (Research TU/e / Graduation TU/e)
Open AccessFile -
A research agenda for active automata learning
Fortz, S. (Corresponding author), Ghassemi, F., Henry, L., Howar, F., Neele, T., Rot, J. & Suilen, M., 19 Feb 2026, (E-pub ahead of print) In: International Journal on Software Tools for Technology Transfer. XXResearch output: Contribution to journal › Article › Academic › peer-review
Open Access
Equipment
Datasets
-
Infinite-data PBES Quotienting with the mCRL2 toolset
Neele, T. (Contributor), Willemse, T. A. C. (Contributor) & Groote, J. F. (Contributor), Zenodo, 4 Nov 2019
Dataset
-
Artifact - Formalisation of a new weak semantics for AuDaLa
Leemrijse, G. (Contributor), Franken, T. T. P. (Contributor) & Neele, T. (Contributor), Zenodo, 5 Jul 2024
DOI: 10.5281/zenodo.12665500, https://zenodo.org/records/12665500
Dataset
-
Artifact - Formalisation of a new weak semantics for AuDaLa
Leemrijse, G. (Contributor), Franken, T. T. P. (Contributor) & Neele, T. (Contributor), Zenodo, 21 Aug 2024
DOI: 10.5281/zenodo.13354543, https://zenodo.org/records/13354543
Dataset
Prizes
-
Best Paper Award FACS 2018
Neele, T. S. (Recipient), Willemse, T. A. C. (Recipient) & Groote, J. F. (Recipient), 11 Oct 2018
Prize: Other › Career, activity or publication related prizes (lifetime, best paper, poster etc.) › Scientific
-
CONCUR 2025 Best Paper Award
Neele, T. (Recipient), Aug 2025
Prize: Other › Career, activity or publication related prizes (lifetime, best paper, poster etc.) › Scientific
-
EATCS Best Paper Award
Neele, T. (Recipient), Valmari, A. (Recipient) & Willemse, T. A. C. (Recipient), 2 Jul 2020
Prize: Other › Career, activity or publication related prizes (lifetime, best paper, poster etc.) › Scientific
-
2020 ICAB Conference
Limburg, A. A. A. (Organiser), Budé, R. H. S. (Organiser), Swagten, H. J. M. (Organiser), van Leeuwen, K. A. H. (Organiser), de Vink, E. P. (Organiser), Gómez Puente, S. M. (Organiser) & Kroesen, G. M. W. (Organiser)
5 Nov 2020Activity: Participating in or organising an event types › Conference › Scientific
-
IPA Herfstdagen on Security (November 21-25,2005), Zwartsluis, The Netherlands
de Vink, E. (Speaker)
22 Nov 2005Activity: Talk or presentation types › Contributed talk › Scientific
Press/Media
-
GLOBAL ROUND UP SECTOR WEEKLY: UNIVERSITY NEWSLETTER OF WEEK-ENDED OCT 29, 2023
30/10/23
1 item of Media coverage
Press/Media: Expert Comment
-
The 17 movies John Carpenter considers “guilty pleasures”
25/08/23
1 item of Media coverage
Press/Media: Expert Comment
-
TU/e Researchers Awarded NWO Veni Grants for Innovative Studies in Diverse Fields
Krishnamoorthy, D., Conijn, R., Fitzgerald, B., Dubslaff, C., Hövelmanns, K. & Moerman, P. G.
4/08/23
1 item of Media coverage
Press/Media: Expert Comment
Student theses
-
Abstracting real-valued parameters in parameterised boolean equation systems
Laveaux, M. (Author), Willemse, T. A. C. (Supervisor 1), 26 Feb 2018Student thesis: Master
File -
A complete axiomatisation for probabilistic trace equivalence
Timmers, F. (Author), Groote, J. F. (Supervisor 1), 26 Nov 2018Student thesis: Master
File -
Adding sequential composition and termination to the linear time: branching time spectrum
Nijland, L. (Author), Luttik, S. P. (Supervisor 1), 31 Aug 2018Student thesis: Master
File