Tools

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.

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.

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

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

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.

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.

Sylvan

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

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.

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.