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 grammarware.net. Engage! is maintained by Vadim Zaytsev.
A benchmark suite for fault tree analysis, available at dftbenchmarks.utwente.nl; 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.
A toolset for quantitative modelling and analysis, see www.modestchecker.net. 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.
A collection of probabilistic and timed benchmark models, available at qcomp.org 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.
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.
- ANIMO: Analysis of Networks with Interactive MOdeling
- Bhave: Simulation of Hybrid Systems
- DFTCalc: Dynamic Fault Tree Calculator (to be integrated with Storm)
- IMCA: Interactive Marcov Chain Analyzer (replaced by Storm)
- JTorX: a Tool for Model-Based Testing
- kimwitu: A Term Processor
- LITE: LOTOS Integrated Tool Environment
- MoonWalker: A Model Checker Developed on the Mono Platform
- MoTor: MoDeST Tool Environment
- MRMC: Markov Reward Model Checker
- ProMoVer: A Tool for Procedure-Modular Verification
- Puptol: Publish Your (Prototype) Tool On-Line
- SCOOP: Symbolic reductions of probabilistic specifications with data
- SLADE: Student LAnguage Development Environment
- SpinJa: A model checker for Promela, written in Java
- TorX: a Tool for Model-Based Testing
- TorXviz: an approach to visualization (used by TorX and JTorX)