Institute of

Theoretical Computer Science


Technische Universität Braunschweig


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!


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 Moby/PEA and its backend PEAtoolkit are model checkers for timed systems. Johannes Faber (University of Oldenburg) is the main developer.