The following software tools have been developed by the FMT group over the recent years. We are still working on these tools and invite you to experiment with them.


An online platform that creates an atelier-like setting that emphasizes collaboration and sharing of ideas. Atelier is described in Ansgar Fehnker, Angelika Mader: Atelier for Creative Programming (CSEDU 2020). Atelier is maintained by Ansgar Fehnker.


A project in language design aimed at creating a language that is, on one hand, small enough to be quickly implementable (fully or partially) within any framework that can support its features, and, on the other hand, complex enough to cover typical problems of legacy language processing. For details, see the BabyCOBOL website. BabyCOBOL is maintained by Vadim Zaytsev.


The only event-based parser generator in existence. A detailed description is at Engage! is maintained by Vadim Zaytsev.


A benchmark suite for fault tree analysis, available at; maintained by Mariëlle Stoelinga and Marijn Peppelman.


GRAT is a SAT solver certificate checking tool chain, which is formally verified using the Isabelle/HOL theorem prover and maintained by Peter Lammich.


GROOVE is all about graph transformation, model transformation, object-oriented verification, behavioural semantics. The tool is maintained by Arend Rensink.


A software verification framework in Isabelle/HOL maintained by Peter Lammich; for details, see its website.


An efficient C library that implements work-stealing (website), maintained by Tom van Dijk.


LTSmin is a high-performance model checker and minimisation tool for models based on labelled transition systems. It is maintained by Tom van Dijk.

The Modest Toolset

A toolset for quantitative modelling and analysis, see It is maintained by Arnd Hartmanns and developed jointly with the Dependable Systems and Software group at Saarland University.


Oink is a parity game solver. It is maintained by Tom van Dijk.

Quantitative Verification Benchmark Set

A collection of probabilistic and timed benchmark models, available at and maintained by Arnd Hartmanns.


Seshat collects and records so-called "test logs". It is being developed by David Huistra.


Sylvan: a parallel C implementation of binary decision diagrams maintained by Tom van Dijk.


UTML allows you to draw graph-like diagrams. It is designed to easily draw diagrams that are used in Technical Computer Science courses at the University of Twente, for example during digital examinations. The tool is maintained by Tim Kemp.


VerCors' job is the verification of concurrent data structures. The tool is developed in a team coordinated by Marieke Huisman.

Not Actively Developed Tools

The following tools have been developed by the FMT group, but that are not longer actively maintained and supported. You are still welcome to use these older tools, though.