Tools
Our tool development is quite active and we regularly offer Bachelor's and Master's theses on improving verification algorithms. If you are interested, get in touch!
FSTTCS 2016 - RIGG
In conjunction with our FSTTCS 2016 submission Summaries for Context-Free Games, we developed the tool RIGG (Regular Inclusion Grammar Games) that can solve context-free grammar games with a regular winning condition. Our prototype implements our algorithm based on Kleene-iteration as well as Cachat's algorithm for solving pushdown games, that can also be used to solve the problem. We compared the algorithms on random-generated examples and were able to show that our algorithm outperforms Cachat by three orders of magnitude. More information and details about the performance evaluation can be found here.VMCAI16 - Pointer Race Freedom
In conjunction with our VMCAI submission Pointer Race Freedom we developed a model checker for proving linearizability of lock-free data structures. Our prototype leverages the novel notion of pointer races to improve the scalability of an existing thread-modular shape analysis. Indeed, we were able to show a speed-up of two orders of magnitude. More information and details about the performance evaluation can be found here.Trencher
Trencher
is a tool for checking and enforcing robustness of assembler programs against the x86-TSO memory model.
The tool was developed jointly by
Egor Derevenetc and
Roland Meyer.
The research was supported by the projects
SDPA: Seismic Development and processing architecture@Fraunhofer
and
ROIS: Robustness under Realistic Instruction Sets@DAAD.
Petruchio
Petruchio
translates structurally stationary networks into Petri nets and analyses the latter harnessing sophisticated backend model checkers for Petri nets as well as novel coverability algorithms.
The core features are explained on this poster.
The tool was developed jointly by Tim Strazny (University of Oldenburg) and Roland Meyer.
Moby/PEA
Moby/PEA and its backend PEAtoolkit are model checkers for timed systems.
Johannes Faber (University of Oldenburg) is the main developer.