Projecten per jaar
Organisatieprofiel
Introductie / missie
Formal System Analysis focuses on theories, techniques and tools for modeling and analyzing the behaviors of software-controlled systems.
Highlighted phrase
Formal analysis is essential for cost-effective, highly reliable software-controlled systems
Organisatieprofiel
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 courses in Logic, Formal Methods, Model Checking, Micro-processor Verification, and Automated Reasoning.
Much of the group’s research is consolidated in tools. Prominent examples include mCRL2 and MaDL. mCRL2 is a process-algebraic language with an award-winning tool set for modeling and analyzing concurrent systems. MaDL is a language with associated verification techniques for scalable liveness verification of micro-architectures of computer processors.
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)
- DEWI: Dependable Embedded Wireless Infrastructure (Artemis project)
Vingerafdruk
Samenwerkingen en hoofdonderzoeksgebieden uit de afgelopen vijf jaar
Profielen
-
Jore J. Booy, Msc
- Mathematics and Computer Science, Formal System Analysis - Promovendus
Persoon: Prom. : Promovendus
-
Mark S. Bouwman
- Mathematics and Computer Science, Formal System Analysis - ex Promovendus
Persoon: Prom. : Promovendus
projecten
- 1 Afgelopen
-
Composable Embedded Systems for Healthcare
Groote, J. F. (Project Manager) & Vlasiou, M. (Projectmedewerker)
1/05/11 → 30/06/17
Project: Onderzoek direct
-
Axiomatising weak bisimulation congruences over CCS with left merge and communication merge
Aceto, L., Castiglioni, V. (Corresponding author), Ingólfsdóttir, A. & Luttik, B., 3 sep. 2025, In: Theoretical Computer Science. 1047, 30 blz., 115325.Onderzoeksoutput: Bijdrage aan tijdschrift › Tijdschriftartikel › Academic › peer review
Open AccessBestand -
Efficient Evidence Generation for Modal µ-Calculus Model Checking
Stramaglia, A. (Corresponderende auteur), Keiren, J. J. A., Laveaux, M. & Willemse, T. A. C., 1 mei 2025, Tools and Algorithms for the Construction and Analysis of Systems: 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3–8, 2025, Proceedings, Part I. Gurfinkel, A. & Heule, M. (uitgave). Springer, blz. 191-210 20 blz. (Lecture Notes in Computer Science (LNCS); vol. 15696).Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review
Open AccessBestand2 Downloads (Pure) -
Efficient Evidence Generation for Modal µ-Calculus Model Checking (extended version)
Stramaglia, A., Keiren, J. J. A., Laveaux, M. & Willemse, T. A. C., 27 jan. 2025.Onderzoeksoutput: Werkdocument › Preprint › Academic
Bestand
Uitrusting
Datasets
-
Decomposing Monolithic Processes using the mCRL2 toolset
Laveaux, M. (Ontwerper) & Willemse, T. A. C. (Ontwerper), Zenodo, 3 jan. 2022
Dataset
-
An O(m log n) Algorithm for Branching Bisimilarity on Labelled Transition Systems
Wijs, A. (Ontwerper), Keiren, J. J. A. (Ontwerper), Groote, J. F. (Ontwerper) & Jansen, D. N. (Ontwerper), Figshare, 20 feb. 2020
DOI: 10.6084/m9.figshare.11876688
Dataset
-
Antichain-based refinement checking benchmark using the mCRL2 toolset
Laveaux, M. (Bijdrager), Zenodo, 19 sep. 2019
Dataset
Prijzen
-
Best Paper Award FACS 2018
Neele, T. S. (Ontvanger), Willemse, T. A. C. (Ontvanger) & Groote, J. F. (Ontvanger), 11 okt. 2018
Prijs: Anders › Werk, activiteit of publicatie gerelateerde prijzen (lifetime, best paper, poster etc.) › Wetenschappelijk
-
EATCS Best Paper Award
Neele, T. (Ontvanger), Valmari, A. (Ontvanger) & Willemse, T. A. C. (Ontvanger), 2 jul. 2020
Prijs: Anders › Werk, activiteit of publicatie gerelateerde prijzen (lifetime, best paper, poster etc.) › Wetenschappelijk
-
FMICS-AVoCS Best Paper award
Groote, J. F. (Ontvanger), Wesselink, J. W. (Ontvanger) & Willemse, T. A. C. (Ontvanger), 20 sep. 2017
Prijs: Anders › Werk, activiteit of publicatie gerelateerde prijzen (lifetime, best paper, poster etc.) › Wetenschappelijk
-
2020 ICAB Conference
Limburg, A. A. A. (Organisator), Budé, R. H. S. (Organisator), Swagten, H. J. M. (Organisator), van Leeuwen, K. A. H. (Organisator), de Vink, E. P. (Organisator), Gómez Puente, S. M. (Organisator) & Kroesen, G. M. W. (Organisator)
5 nov. 2020Activiteit: Types deelname aan of organisatie van een evenement › Congres › Wetenschappelijk
-
IPA Herfstdagen on Security (November 21-25,2005), Zwartsluis, The Netherlands
de Vink, E. (Spreker)
22 nov. 2005Activiteit: Types gesprekken of presentaties › Aangemelde presentatie › Wetenschappelijk
-
VVSS 2004 (Verification and Validation of Software Systems), LaQuSo, Eindhoven, The Netherlands
Romijn, J. (Spreker)
24 nov. 2004Activiteit: Types gesprekken of presentaties › Aangemelde presentatie › Wetenschappelijk
Scripties/Masterproeven
-
Abstracting real-valued parameters in parameterised boolean equation systems
Laveaux, M. (Auteur), Willemse, T. A. C. (Afstudeerdocent 1), 26 feb. 2018Scriptie/Masterproef: Master
Bestand -
A complete axiomatisation for probabilistic trace equivalence
Timmers, F. (Auteur), Groote, J. F. (Afstudeerdocent 1), 26 nov. 2018Scriptie/Masterproef: Master
Bestand -
Adding sequential composition and termination to the linear time: branching time spectrum
Nijland, L. (Auteur), Luttik, S. P. (Afstudeerdocent 1), 31 aug. 2018Scriptie/Masterproef: Master
Bestand