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.

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

Tomorrow, 12:30, Zi 5126Lunch colloqium: Paul Bonsma: Tight Lower and Upper Bounds for the Complexity of Canonical Color Refinement

More events.

Press Releases and Media Coverage

Jan 19, 2013

Opinion article Mariëlle Stoelinga in Trouw because Problems with Dutch emergency number 112: Aan nummer 112 mag je eisen stellen. [in Dutch]

Dec 13, 2012

Article on ANIMO project by Stefano Schivo in I/O VIVAT: Modeling biology with ANIMO. [in English]

Nov 07, 2012

Article on TREsPASS project in Bits & Chips: UT en partners leggen zwakheden in informatiebeveiliging bloot. [in Dutch]

More press releases and media coverage.

Latest News

May 01, 2013

Joost-Pieter Katoen appointed RWTH Distinguished Professor

RWTH Aachen has selected Prof. Joost-Pieter Katoen as Distinguished Professor. This competitive reward is an exceptional recognition of his excellent research record. The honour comes with an extensive research budget.

Feb 26, 2013

Lesley Wevers, Wanno Drijfhout and Oliver Jundt won Norvig Web Data Science Award

Lesley Wevers, Wanno Drijfhout and Oliver Jundt have won the Norvig Web Data Science Award. This is a challenge where participants show what they can do with the Common Crawl dataset -- a snapshot of a large part of the web -- using SURFsara’s Hadoop service to provide big data compute power. The winning entry uses the dataset to construct a database of associated concepts, which can be queried through a web application with two query interfaces. A textual interface allows searching for similarities and differences between multiple concepts using a query language similar to set notation, and a graphical interface allows users to visualize similarity relationships of concepts in a force directed graph.

For more information see:
Norvig award website: http://norvigaward.github.com/
Winning Entry: http://norvigaward.github.com/entries.html#naward13
Web application: http://traitor.imperamus.eu/

Dec 12, 2012

Arend Rensink nominated for the Inter-Actief Onderwijsprijs 2012

For the second year running, Arend Rensink of the FMT group was nominated by the Computer Science students as one of the potential recipients of the yearly award for the best teacher. The list of nominees, in alphabetical order, reads:

  • Harry Aarts
  • Lesley Broos
  • Bert Molenkamp
  • Arend Rensink

See also here.

More news.

Latest Publications

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

Amighi, A. and Blom, S.C.C. and Huisman, M. (2013) Resource protection using atomics: patterns and verifications. Technical Report TR-CTIT-13-10, Centre for Telematics and Information Technology, University of Twente, Enschede. ISSN 1381-3625

Gurov, D. and Huisman, M. (2013) Reducing Behavioural to Structural Properties of Programs with Procedures. Theoretical computer science, 480. pp. 69-103. ISSN 0304-3975 *** ISI Impact 0,665 ***

Katoen, J.P. and Peled, D. (2013) Taming confusion for modeling and implementing probabilistic concurrent systems. In: Proceedings of the 22nd European Symposium on Programming (ESOP 2013), 16-24 Mar 2013, Rome, Italy. pp. 411-430. Lecture Notes in Computer Science 7792. Springer Verlag. ISSN 0302-9743 ISBN 978-3-642-37035-9

Timmer, M. and van de Pol, J.C. and Stoelinga, M.I.A. (2013) Confluence reduction for Markov automata. In: Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013), 23-24 Mar 2013, Rome, Italy. 18. University of Trieste. ISBN not assigned

Hartmanns, A. and Timmer, M. (2013) On-the-fly confluence detection for statistical model checking. In: Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013), 23-24 Mar 2013, Rome, Italy. 19. University of Trieste. ISBN not assigned

More publications.