Tim Willemse is an Associate Professor in the Formal System Analysis group of the Model Driven Software Engineering section in the Department of Mathematics and Computer Science at Eindhoven University of Technology (TU/e). Tim’s research focuses on applying, developing and scaling formal methods for designing correct and reliable systems. His research receives financial support from organizations such as NWO and the European Commission, and commercial parties, including ASML, Océ and Verum.
His group works on algorithms and theory for parity games and fixpoint logics, such as parameterised Boolean equation systems, and their application. Their theories and algorithms drive the model checking technology offered by mCRL2, a toolset for specifying and analyzing (software controlled) systems.
Tim led the development of dedicated verification tooling for the software controlling the physics experiments at CERN. More recently, he developed the verification technology underlying the commercial model-driven software engineering toolset Dezyne, used on a day-to-day basis by the high-tech industry.
Tim Willemse received his PhD and MSc in Computer Science from TU/e. In addition to his position at TU/e, Tim has a part-time affiliation with CERN, as a software engineer and researcher. He has also worked as a researcher at ASML and Radboud University, Nijmegen, the Netherlands. In both positions, he worked on Model-Based Testing techniques. Until December 2017, Tim was managing director of the national research school IPA. He is also a member of the Next Gen Board of the HTSC, and of the societies ACM SIGACT, ACM SIGLOG, EATCS, NVTI, IPA.
Tim has been involved in a wide range of research projects, including NWO-TOP project AVVA, a project on exploring the use of massive parallelism to speed up verification and the use of verification to assess the correctness of parallel programs. He was project leader on FP7 TTP VICTORIA, a project exploring the connection between the industrial language Dezyne and mCRL2, on the NWO project VOCHS, (verification of control software of the CMS experiment at the Large Hadron Collider) and on the NWO-project COMFORTS (verification of data-dependent and real-time systems).
Correct and efficient antichain algorithms for refinement checkingFormal Techniques for Distributed Objects, Components, and Systems (2019)
Correct and efficient antichain algorithms for refinement checkingarXiv (2019)
Correct and efficient antichain algorithms for refinement checking(2019)
The mCRL2 toolset for analysing concurrent systems25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019 (2019)
Solving parameterised boolean equation systems with infinite data through quotienting15th International Conference on Formal Aspects of Component Software, FACS 2018 (2018)
- Process theory
- Algorithms for model checking
- Seminar formal system analysis
- Automotive software engineering
No ancillary activities