Formal Methods and Tools

In the Formal Methods and Tools (FMT) research group, formal techniques and tools are developed and used as a means to support the development of software. This includes the development of formal theories of concurrency, design methodologies for distributed systems, and correctness assessment using verification or validation techniques. The group is also concerned with the development of traditional tools such as compilers and interpreters. In both research and courses much attention is paid to the applicability of formal methods.

The FMT group is part of the Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) at the University of Twente. The FMT group also participates in the research institute CTIT.

Upcoming Events (for recurrent events only next 7 days are shown)

Tuesday, 12:30, HB 2BLunch colloqium: Jeroen Meijer: Title to be announced
Jul 13, 16:30, Waaier 3PhD Defense: Tom van Dijk: Sylvan: Multi-core Decision Diagrams

More events; more lunch colloquia.

Press Releases and Media Coverage

Dec 10, 2015

Article mentioning Marieke Huisman: Hour of Code: Hoe leer je programmeren?. [in Dutch]

Oct 09, 2015

Article mentioning our Nature Nano paper in Gizmag: "Designless" brain-like chips created through artificial evolution. [in English]

Oct 08, 2015

Article mentioning news and views on the achievements of our publication in Nature Nanotechnology: Computing: Naturally random. [in English]

More press releases and media coverage.

Latest News

Apr 06, 2016

Marielle Stoelinga and Marcus Gerhold win best paper award at ETAPS 2016

During the Euopean Joint Conferences on Theory and Practice and Software 2016 (ETAPS'16) in Eindhoven Mariëlle Stoelinga and Marcus Gerhold win the EASST best paper for their paper titled 'Model-Based Testing of Probabilistic Systems'. 

Their work describes the testing process of systems that make use of probability and how to check whether or not they were implemented correctly.

Further information.
Apr 06, 2016

Results announced for the VerifyThis 2016 Program Verification Competition, co-organised by Marieke Huisman

VerifyThis 2016 is a program verification competition taking place as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2016) on April 2-3, 2016 in Eindhoven, the Netherlands. It is the 5th event in the VerifyThis competition series.


  • Best problem submission: Daniel Grahl, for suggesting "Strassen's algorithm", which inspired the matrix multiplication challenge.
  • Distinguished user-assistance tool feature: Alexander J. Summers and Malte Schwerhoff (Viper) for their support of quantified permissions.
  • Best student team (2x): Martin Clochard (Why3), Léon Gondelman & Mário Pereira (Why3)
  • Best team: Bart Jacobs (VeriFast)


More information:


Apr 05, 2016

Arnd Hartmanns wins GI/ITG MMB Dissertation Award

The GI/ITG Technical Committee of "Measurement, Modelling and Evaluation of Computing Systems" has awarded to Arnd Hartmanns the MMB Dissertation Award 2016 at the biennial MMB & DFT conference in Münster on April 5, 2016.

Arnd Hartmanns completed his Ph.D. with a thesis titled "On the Analysis of Stochastic Timed Systems" at Saarland University, Germany, supervised by Prof. Holger Hermanns. He joined the Formal Methods and Tools Group at the University of Twente as a postdoc in October 2015.

More news.

Latest Publications

(note: 'latest' refers to the date of addition to the EPrints publication database, not to the date of publication.)

Ahmad, W. and Jongerden, M.R. and Stoelinga, M.I.A. and van de Pol, J.C. (2016) Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata (extended version). Technical Report TR-CTIT-16-03, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625

Greff, K. and van Damme, R.M.J. and Koutnik, J. and Broersma, H.J. and Mikhal, J. and Lawrence, C.P. and van der Wiel, W.G. and Schmidhuber, J. (2016) Unconventional computing using evolution-in-nanomaterio: neural networks meet nanoparticle networks. In: The Eighth International Conference on Future Computational Technologies and Applications, FUTURE COMPUTING 2016, 20-24 March 2016, Rome, Italy. pp. 15-20. IARIA International Academy, Research and Industry Association. ISBN 978-1-61208-461-9

Rensink, A. (2016) Verification Techniques for Graph Rewriting (Tutorial). (Invited) In: Verification of Evolving Graph Structures, 1-6 Nov 2015, Dagstuhl, Germany. pp. 18-18. Dagstuhl Reports 5 (11). Dagstuhl Publishing. ISSN 2192-5283

Zhang, Y. and Broersma, H.J. and Chen, Y. (2016) Narrowing down the gap on cycle-star Ramsey numbers. Journal of combinatorics, 7 (2-3). pp. 481-493. ISSN 2156-3527

Schivo, S. and Degeling, K. and Koffijberg, H. and IJzerman, M.J. and Langerak, R. (2015) PRM113 - Timed Automata Modeling of The Personalized Treatment Decisions In Metastatic Castration Resistant Prostate Cancer. In: ISPOR 18th Annual European Congress Research Abstracts, 7-11 Nov 2015, Milan, Italy. A702-A703. Value in Health 18 (7). International Society for Pharmacoeconomics and Outcomes Research (ISPOR). ISSN 1098-3015

More publications.