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. Formal methods are mathematical techniques for the construction and analysis of software systems. Our central goal is to increase the reliability of the software that we rely on, as individuals and as society. We primarily target complex concurrent ICT systems, embedded in a technological context or in a distributed environment.

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)

Tomorrow, 12:30, Hal B 2BLunch colloqium: Saeed Darabi: A Verification Technique for Deterministic Parallel Programs

More events; more lunch colloquia.

Press Releases and Media Coverage

Apr 13, 2017

Press Release Joost-Pieter Katoen in UT nieuws because Eredoctoraat voor Joost-Pieter Katoen: Eredoctoraat voor Joost-Pieter Katoen. [in Dutch]

Mar 30, 2017

Article mentioning Dennis Guck, Mariëlle Stoelinga in Electronic Component News because PhD defense of Dennis Guck: Fewer Malfunctions And Lower Costs Thanks To Smarter Maintenance Model. [in English]

Mar 28, 2017

Press Release Dennis Guck, Mariëlle Stoelinga, Joost-Pieter Katoen because PhD defense of Dennis Guck: Minder storingen en lagere kosten door slimmer onderhoudsmodel. [in Dutch]

More press releases and media coverage.

Latest News

Apr 13, 2017

Eredoctoraat Universiteit Aalborg voor Joost-Pieter Katoen

Op 7 april jl. heeft Joost-Pieter Katoen, deeltijd hoogleraar bij de vakgroep Formal Methods and Tools, een eredoctoraat van de Universiteit van Aalborg in ontvangst genomen.

Joost-Pieter krijgt het eredoctoraat vanwege zijn distinguished efforts in computer science.

 

Further information.
Feb 20, 2017

'Vici'-beurs voor Marieke Huisman

Marieke Huisman (CTIT) is hoogleraar Software Reliability. Zij ontwikkelt nieuwe technieken om steeds complexer wordende software betrouwbaar te maken en te houden.

Dankzij de Vici-subsidie van 1,5 miljoen Euro kan prof.dr. Marieke Huisman vijf jaar onderzoek doen naar betrouwbare software. Het maken van betrouwbare software blijft een grote uitdaging. Wanneer je programmeert, schrijf je eigenlijk instructies die te begrijpen zijn voor een computer. In het verleden werden deze instructies één voor één uitgevoerd. Tegenwoordig is het niet ongebruikelijk dat een computer meerdere series instructies gelijktijdig uitvoert. Dit vergroot de complexiteit van het proces en daarmee de kans op fouten of problemen. Huisman ontwikkelt nieuwe technieken waarmee zulke complexe stukken programmeerwerk gecontroleerd worden op instructies die fouten of conflicten gaan veroorzaken nog vóórdat je de instructies daadwerkelijk probeert uit te voeren in je productieomgeving. Op deze manier weet je of de programmeercode foutloos werkt, voordat je deze op de eindbestemming inzet.

De Vici subsidie is toegekend door de Nederlandse Organisatie voor Wetenschappelijk Onderzoek NWO.

Further information.
Nov 11, 2016

Vincent Bloemen wins Best Presentation Award at the FM 2016 Doctoral Symposium

During the Doctoral Symposium of the 21st International Symposium on Formal Methods (FM 2016) in Cyprus, Vincent Bloemen won the Best Presentation Award for his paper titled 'Parallel Model Checking of ω-Automata'.

He presented ideas on how he attempts to improve the model checking procedure by investigating different types of ω-automata such as Büchi, Rabin and Parity, and developing efficient parallel algorithms for checking such automata.

Further information.

More news.

Latest Publications

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

Gomes, P. and Gurov, D. and Huisman, M. (2016) Specification and Verification of Synchronization with Condition Variables. In: Proceedings of the Fifth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016), November 14, 2016, Tokyo, Japan. pp. 3-19. Communications in Computer and Information Science 694. Springer Verlag. ISSN 1865-0929 ISBN 978-3-319-53946-1

Neele, T. and Wijs, A. and Bosnacki, D. and van de Pol, J.C. (2016) Partial-Order Reduction for GPU Model Checking. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, 17-20 Oct 2016, Chiba, Japan. pp. 357-374. Lecture Notes in Computer Science 9938. Springer Verlag. ISSN 0302-9743 ISBN 978-3-319-46519-7

Geske, M. and Jasper, M. and Steffen, B. and Howar, F. and Schordan, M. and van de Pol, J.C. (2016) RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification. In: Proceedings of the 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (II), ISoLA 2016, 10-14 Oct 2016, Corfu, Greece. pp. 787-803. Lecture Notes in Computer Science 9953. Springer Verlag. ISSN 0302-9743 ISBN 978-3-319-47168-6

van Dijk, T. and van de Pol, J.C. (2016) Multi-core Symbolic Bisimulation Minimisation. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), 2-8 April 2016, Eindhoven, The Netherlands. pp. 332-348. Lecture Notes in Computer Science 9636. Springer Verlag. ISSN 0302-9743 ISBN 978-3-662-49673-2

Junges, S. and Guck, D. and Katoen, J.P. and Rensink, A. and Stoelinga, M.I.A. (2017) Fault trees on a diet: automated reduction by graph rewriting. Formal Aspects of Computing, online pre-publication. pp. 1-53. ISSN 0934-5043 *** ISI Impact 0,521 ***

More publications.