Formal Methods and Tools

The mission of FMT is to develop mathematical methods and high-performance algorithms for the design of reliable software- and data-intensive control systems. We focus on modelling, synthesis, analysis, and prediction of their functional, structural and quantitative aspects. We aim to understand a complex systems’ safety, reliability, performance, energy usage, and the risks and costs associated to its architecture, design, operation and maintenance.

Our mission builds on extensive experience in concurrency theory, static analysis, theorem proving, model checking, and term/graph rewriting. Our focus areas are:

  1. Quantitative modelling and analysis for cyber-physical and socio-technical systems;
  2. Program verification for concurrent and distributed software;
  3. High-performance algorithms and tools for model checking and model transformation.

Latest News

May 16, 2019

NWO Open Technology Programme grant for Marieke Huisman (University of Twente) and Anton Wijs

Prof.dr. M. Huisman (University of Twente) and dr. A. Wijs received an NWO OTP grant for the project “ChEOPS: verified Construction of corrEct and Optimised Parallel Software”. Two PhD students will be appointed, one in Twente and one in Eindhoven, to make the development and maintenance of software aimed at graphics processing units (GPUs) more insightful and effective in terms of functional correctness and performance.

GPUs have an increasingly big impact on industry and academia, due to their great
computational capabilities. However, in practice, one usually needs to have expert knowledge on GPU architectures to optimally gain advantage of those capabilities. At the Eindhoven University of Technology, Wijs will work on modelling GPU applications using a Domain Specific Language, formally verifying the correctness of the models, and automatically generating GPU code. At the University of Twente, Huisman will work on the structured optimisation of GPU code, while ensuring that functional correctness is preserved. Existing formal verification techniques, model checking and code verification, will be combined to create, for the first time, a complete end-to-end development workflow for GPU applications.

To ensure the practical effectiveness of the resulting workflow, a users committee, consisting of SURFsara, the Netherlands eScience Center, Stream HPC, and CodePlay (UK), will provide real-life cases and provide feedback throughout the project.

April 15, 2019

VerifyThis awards for VerCors teams!

At “VerifyThis 2019”, part of the ETAPS conference in Prague in April 2019, several prizes were won by FMT members.
Firstly, Sophie Lathouwers and Wytse Oortwijn won the Best Student Team award!
Secondly, Marieke Huisman and Sebastiaan Joosten won the “Most Distinguished Tool Feature” for their usage of ghost method parameters to model sparse matrices!

Feb. 1, 2019

First and second prize VERSEN Master thesis award for FMT theses

During the 5th National Symposium Software Engineering held on February 1, 2019 the first VERSEN Master thesis awards have been handed out. All theses were judged for: nvovelty to and impact in the field of software research, timeliness, quality of the thesis report and associated artifacts, and methodological approach and execution.

The first prize was awarded to Djurre van der Wal for his thesis "Translating AWN networks to the mCRL2 model checker", supervised by Jaco van de Pol, Ansgar Fehnker, Peter Höfner, and Rob van Glabbeek. 

The second prize was awarded to Jan-Jelle Kester for his thesis "CheckMerge: a system for risk assessment of code merges", supervised by Marieke Huisman.