• Groene Loper 5, Metaforum

    5612 AP Eindhoven

    Nederland

  • P.O. Box 513, Department of Mathematics and Computer Science

    5600 MB Eindhoven

    Nederland

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

Over de organisatie

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 Verdiep u in de onderzoeksgebieden waarop Formal System Analysis actief is. Deze onderwerplabels komen uit het werk van de leden van deze organisatie. Samen vormen ze een unieke vingerafdruk.

  • Netwerk Recente externe samenwerking op landenniveau. Duik in de details door op de stippen te klikken.

    Onderzoeksoutput

    A formal actor-based model for streaming the future

    Azadbakht, K., de Boer, F. S., Bezirgiannis, N. & de Vink, E., 1 feb 2020, In : Science of Computer Programming. 186, 22 blz., 102341.

    Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

  • Finding compact proofs for infinite-data parameterised Boolean equation systems

    Neele, T., Willemse, T. A. C. & Groote, J. F., 1 mrt 2020, In : Science of Computer Programming. 188, 22 blz., 102389.

    Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

  • 1 Citaat (Scopus)

    Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems

    Neele, T., Willemse, T. A. C. & Wesselink, W., 17 apr 2020, Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part II. Biere, A. & Parker, D. (redactie). Springer, blz. 307-324 18 blz. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12079 LNCS).

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    Open Access
  • Prijzen

    Best Paper award

    S.P. Luttik (Ontvanger) & Tim A.C. Willemse (Ontvanger), 4 sep 2018

    Prijs: AndersWerk, activiteit of publicatie gerelateerde prijzen (lifetime, best paper, poster etc.)Wetenschappelijk

    Best Paper award

    J.F. Groote (Ontvanger), J.W. Wesselink (Ontvanger) & Tim A.C. Willemse (Ontvanger), 20 sep 2017

    Prijs: AndersWerk, activiteit of publicatie gerelateerde prijzen (lifetime, best paper, poster etc.)Wetenschappelijk

  • Best Paper Award FACS 2018

    T.S. Neele (Ontvanger), Tim A.C. Willemse (Ontvanger) & J.F. Groote (Ontvanger), 11 okt 2018

    Prijs: AndersWerk, activiteit of publicatie gerelateerde prijzen (lifetime, best paper, poster etc.)Wetenschappelijk

    Activiteiten

    • 1 Aangemelde presentatie

    IPA Herfstdagen on Security (November 21-25,2005), Zwartsluis, The Netherlands

    Erik de Vink (Spreker)
    22 nov 2005

    Activiteit: Types gesprekken of presentatiesAangemelde presentatieWetenschappelijk

    Knipsels

    Introduction to Type Theory.pdf

    J.H. Geuvers

    13/05/18

    1 item van Media-aandacht

    Pers / media: Vakinhoudelijk commentaar

    EIT Digital launches three additional IoT MOOCs on Coursera

    J.F. (Jan Friso) Groote

    28/11/1630/11/16

    38 items van Media-aandacht

    Pers / media: Vakinhoudelijk commentaar

    New Developments in Model Driven Software Engineering

    J.F. (Jan Friso) Groote

    24/06/15

    1 item van Media-aandacht

    Pers / media: Vakinhoudelijk commentaar

    Scripties/Masterproeven

    Abstracting real-valued parameters in parameterised boolean equation systems

    Auteur: Laveaux, M., 26 feb 2018

    Begeleider: Willemse, T. (Afstudeerdocent 1)

    Scriptie/masterproef: Master

    Bestand

    A complete axiomatisation for probabilistic trace equivalence

    Auteur: Timmers, F., 26 nov 2018

    Begeleider: Groote, J. F. (Afstudeerdocent 1)

    Scriptie/masterproef: Master

    Bestand

    Adding sequential composition and termination to the linear time: branching time spectrum

    Auteur: Nijland, L., 31 aug 2018

    Begeleider: Luttik, S. (Afstudeerdocent 1)

    Scriptie/masterproef: Master

    Bestand