Some open source projects I am involved with.


veriT is an open source SMT (Satisfiability Modulo Theories) solver. It is quite lightweight and depends only on the GMP library. VeriT supports the theories uninterpreted functions and linear arithmetic on the reals and integers. Some other theories are supported in an experimental fashion. Quantifiers are also supported reasonably well. Furthermore, veriT can produce really nice proofs.

As part of my PhD research I am one of the core developers of veriT. For more information on the project see the veriT website.


The QBFToys are a set of tools to convert QBF and DQBF problems into higher order problems in TPTP THF format. They can also perform some normalization. Furthermore, experimental SMT-LIB2 output is implemented. [GitHub]


Dotrace is a tiny library which allows users to trace function calls during the execution of a C program by utilizing GCCs instrument-functions functionality. [Inria GitLab]


This is a simple library to render Haiku Vector Icons. Writing in C only and currently only depending on Cairo, this library makes it possible to render the tiny vector images outside the Haiku ecosystem. [Git at Beepboop Network]