If you made any changes in Pure these will be visible here soon.

Personal profile

Quote

“The beauty and power of formal software analysis never cease to surprise.”

Research profile

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. 

Academic background

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).

Network Recent external collaboration on country level. Dive into details by clicking on the dots.

Research Output 1999 2019

Correct and efficient antichain algorithms for refinement checking

Laveaux, M., Groote, J. F. & Willemse, T. A. C., 26 Feb 2019, In : arXiv. 28 p., 1902.09880

Research output: Contribution to journalArticleAcademic

Open Access
File
Specifications
Data storage equipment
Experiments

Correct and efficient antichain algorithms for refinement checking

Laveaux, M., Groote, J. F. & Willemse, T., 29 May 2019, Formal Techniques for Distributed Objects, Components, and Systems 39th IFIP WG 6.1 International Conference, FORTE 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019, Proceedings. Pérez, J. & Yoshida, N. (eds.). Cham: Springer, p. 185-203 19 p. (Lecture Notes in Computer Science; vol. 11535)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Antichain
Refinement
Correctness
Divergence
Specification

Correct and efficient antichain algorithms for refinement checking

Laveaux, M., Groote, J. F. & Willemse, T., 2019, Eindhoven: Technische Universiteit Eindhoven. 28 p. (Computer science reports; vol. 19/01)

Research output: Book/ReportReportAcademic

Open Access
File
Specifications
Data storage equipment
Experiments
1 Citation (Scopus)

The mCRL2 toolset for analysing concurrent systems: improvements in expressivity and usability

Bunte, O., Groote, J. F., Keiren, J. J. A., Laveaux, M., Neele, T., de Vink, E. P., Wesselink, W., Wijs, A. & Willemse, T. A. C., 1 Jan 2019, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Vojnar, T. & Zhang, L. (eds.). Cham: Springer, p. 21-39 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11428 LNCS)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Open Access
File
Concurrent Systems
Graphical user interfaces
Usability
Software Product Lines
Domain-specific Languages

A comparison of BDD-based parity game solvers

Sanchez, L., Wesselink, W. & Willemse, T. A. C., 7 Sep 2018, Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification. Waterloo: Open Publishing Association, p. 103-117 15 p. (Electronic Proceedings in Theoretical Computer Science ; vol. 27)

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Open Access

Prizes

Best Paper award

Bas Luttik (Recipient) & Tim Willemse (Recipient), 4 Sep 2018

Recognition: OtherCareer, activity or publication related prizes (lifetime, best paper, poster etc.)Scientific

Best Paper award

Jan Friso Groote (Recipient), Wieger Wesselink (Recipient) & Tim Willemse (Recipient), 20 Sep 2017

Recognition: OtherCareer, activity or publication related prizes (lifetime, best paper, poster etc.)Scientific

Modeling languages

Best Paper Award FACS 2018

Thomas Neele (Recipient), Tim Willemse (Recipient) & Jan Friso Groote (Recipient), 11 Oct 2018

Recognition: OtherCareer, activity or publication related prizes (lifetime, best paper, poster etc.)Scientific

Activities 2000 2000

  • 1 Workshop, seminar, course or exhibition

5th International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS 2000)

Tim Willemse (Organiser)
3 Apr 2000

Activity: Participating in or organising an event typesWorkshop, seminar, course or exhibitionScientific

Courses

Algorithms for model checking

1/09/15 → …

Course

Automotive software engineering

1/09/13 → …

Course

Process theory

1/09/18 → …

Course

Seminar formal system analysis

1/09/14 → …

Course

Student theses

Abstracting real-valued parameters in parameterised boolean equation systems

Author: Laveaux, M., 26 Feb 2018

Supervisor: Willemse, T. (Supervisor 1)

Student thesis: Master

File

A symbolic approach to PBES instantiation

Author: Boshoven, T., 25 Sep 2015

Supervisor: Willemse, T. (Supervisor 1)

Student thesis: Master

File

Black-box random testing of the mCRL2 toolset using attribute grammars

Author: Geelen, M., 31 Mar 2014

Supervisor: Wesselink, J. (Supervisor 1) & Willemse, T. (Supervisor 2)

Student thesis: Master

File

Consistent consequences formalized

Author: van Delft, M., 31 Aug 2016

Supervisor: Willemse, T. (Supervisor 1)

Student thesis: Master

File