Formal System Analysis

  • AddressShow on map

    MetaForum, 6th floor (building 5), Groene Loper 5

    5612AP Eindhoven

    Netherlands

  • Postal addressShow on map

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

    5600MB Eindhoven

    Netherlands

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.

 

 

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.
View full 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
Explore network further
View all 31 researchers

  • Compiling Binary Decision Diagrams with Interrupt-Based Downsizing

    Dubslaff, C. (Corresponding author) & Wirtz, J. (Corresponding author), 2025, Principles of Verification: Cycling the Probabilistic Landscape: Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday. Jansen, N., Junges, S., Kaminski, B. L., Matheja, C., Noll, T., Quatmann, T., Stoelinga, M. & Volk, M. (eds.). Springer, Vol. 3. p. 252-273 22 p. (Lecture Notes in Computer Science; vol. 15262 LNCS).

    Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

  • Formalisation of a New Weak Semantics for AuDaLa

    Leemrijse, G. P., Franken, T. T. P. & Neele, T. (Corresponding author), 12 Feb 2025, Automated Technology for Verification and Analysis: 22nd International Symposium, ATVA 2024, Kyoto, Japan, October 21–25, 2024, Proceedings, Part II. Akshay, S., Niemetz, A. & Sankaranarayanan, S. (eds.). Cham: Springer, p. 93-116 24 p. (Lecture Notes in Computer Science (LNCS); vol. 15055).

    Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

  • Formal Methods in Industry

    ter Beek, M. H. (Corresponding author), Chapman, R., Cleaveland, R., Garavel, H., Gu, R., ter Horst, I., Keiren, J. J. A., Lecomte, T., Leuschel, M., Rozier, K. Y., Sampaio, A., Seceleanu, C., Thomas, M., Willemse, T. A. C. & Zhang, L., Mar 2025, In: Formal Aspects of Computing. 37, 1, p. 1-38 38 p., 7.

    Research output: Contribution to journal › Article › Academic › peer-review

    Open Access
    File
    8 Citations (Scopus)
    17 Downloads (Pure)
View all 1504 research outputs
View all 22 datasets
View all 8 prizes
  • 2 Contributed talk
  • 1 Conference
View all 69 student theses