The following software tools and datasets have been developed and collected by the FMT group over the recent years. We are still working on these tools and datasets and invite you to experiment with them.
BabyCOBOL
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.
EduApps Lab
Development and maintainenance of education supporting (web)apps used within EEMCS. For more information see https://labs.apps.utwente.nl/.
These tools are not FMT-specific, but maintenance is currently placed within FMT.
Engage!
The only event-based parser generator in existence. Engage! is open source and is maintained by Vadim Zaytsev at https://github.com/raincodelabs/engage.
Failure data sets
PrimaVera data: https://primavera-project.com/open-source-datasets/
This website collects a number of data sets on component failure behaviour
Fault tree visualizations
This website explains fault tree models and provides several visualization techniques
FFORT
A benchmark suite for fault tree analysis, available at dftbenchmarks.utwente.nl; maintained by Mariëlle Stoelinga and Marijn Peppelman.
GRAT
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
GROOVE is all about graph transformation, model transformation, object-oriented verification, behavioural semantics. The tool is maintained by Arend Rensink.
Isabelle-LLVM
A software verification framework in Isabelle/HOL maintained by Peter Lammich; for details, see its website.
KNOR
Knor implements reactive synthesis of specifications given by deterministic parity automata to Boolean circuits. See on Github. Knor has won the PGAME track of SYNTCOMP several times. Knor is maintained by Tom van Dijk.
Lace
Lace is an efficient C library that implements fine-grained fork-join work-stealing, maintained by Tom van Dijk.
LRAT-ISA
LRAT-ISA is a fast and verified UNSAT certificate checker. It is as fast as state-of-the-art unverified tools. Using the LRUP format, it can be run in parallel to the SAT solver with little overhead. The verification is done wrt. a grammar of the DIMACS CNF format and a straightforward semantics of CNF formula, and down to the LLVM code implementing the checker.
LTSmin
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 www.modestchecker.net. It is maintained by Arnd Hartmanns and developed jointly with the Dependable Systems and Software group at Saarland University.
Oink
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 qcomp.org and maintained by Arnd Hartmanns.
SAFEST
SAFEST is a tool for the analysis of Dynamic Fault Trees, commercialized by DGB Technologies. The tool implements over 10 years of research on fault tree analysis. SAFEST is based on STORM, and co-funded by the NWO valorization grant TREEFRUIT by Joost-Pieter Katoen, Marielle Stoelinga and Matthias Volk.
Storm
Storm is a model checker for probabilistic models mainly developed at RWTH Aachen University. Contributions from the FMT group include Monte Carlo simulation for dynamic fault trees. Internally, Storm uses Sylvan (see below), which has also been developed at FMT. Other contributions were made by Marijn Peppelman and Matthias Volk.
Sylvan
Sylvan: a parallel C implementation of binary decision diagrams maintained by Tom van Dijk.
UTML
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. It is part of the EduApps lab, see also https://labs.apps.utwente.nl/.
VerCors
The VerCors verifier is a tool for deductive verification of concurrent and parallel software. VerCors can reason about programs written in different programming languages, such as Java, C and OpenCL, where the specifications are written in terms of pre-post-condition contracts using permission-based separation logic. VerCors is able to reason about data-race freedom, memory safety, and functional correctness, and it has been applied on several realistic case studies.
Several tools are being developed directly on top of VerCors by encoding their input languages to VerCors' internal representation, allowing reuse of the existing infrastructure for verification. These tools are Alpinist, Vesuv, and VeyMont.
Alpinist
Alpinist is an annotation-aware GPU program optimizer. Alpinist takes an annotated GPU program and applies an optimization to both the GPU program as well as its annotations. The annotations are transformed in a way that preserves the provability of the resulting optimized GPU program. Alpinist has support for six frequently-used GPU program optimizations, namely loop unrolling, tiling, kernel fusion, iteration merging, matrix linearization and data prefetching.
Vesuv
VeSUV is a transformation tool that encodes embedded systems designs written in the hardware/software co-design language SystemC into PVL, the internal language of VerCors. It creates an encoding of both the design and the SystemC scheduling semantics to generate a PVL program that is semantically equivalent to the original SystemC design. VeSUV also generates basic specifications for the encoded program. The user can then add further specifications and verify them normally with VerCors.
VeyMont
VeyMont is a deductive verification tool for parallel programs. It can check functional correctness and deadlock freedom of so-called "choreographic programs", in which a program is expressed for not just one thread, but for all threads simultaneously. In addition, VeyMont can generate Java code, such that the choreographic program can be run in a distributed manner. Support for verifying the choreographic program after translating it to one specific thread, as well as allowing the user to customize the handling of permissions, is actively being developed.
WAGon
WAGon is a Rust library and ecosystem for working with Weighted Attribute Grammars. WAGs are an active research direction explored by Marcus Gerhold and Vadim Zaytsev, and WAGon is an implementation started by Rafael Dulfer in collaboration with them. It is currently being extended to support communication with smart objects in the context of the Internet of Things, as well as for integrating with more sophisticated machine learning algorithms.
Not Actively Developed Tools within FMT
The following tools have been developed by the FMT group, but are no longer actively maintained and supported by members of the FMT staff. You are still welcome to use these tools, though.
- ANIMO: Analysis of Networks with Interactive MOdeling
- Atelier for Creative Programming (CSEDU 2020)
- 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)