Formal System Analysis

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.