In my research, since 2015, I engage in the development of the verification tool DIVINE. It is a modern, explicit-state model checker. Based on the LLVM toolchain, it can verify programs written in multiple real-world programming languages, including C and C++. The verification core is built on a foundation of high­-per­for­mance algorithms and data structures, scaling all the way from a laptop to a high-end cluster. Discover more on the project website.

LART: LLVM Abstraction & Refinement Tool

The results of my Ph.D. research I mainly part of LART: an LLVM instrumentation framework suited for verification tools to integrate techniques like symbolic execution and abstract interpretation techniques.

It is an instrumentation engine that leverages the Clang toolchain to synthesize code that performs abstract execution. To minimize its impact on the original bitcode, LART uses a combination of dataflow, taint, and alias analyses.

It is currently developed as part of DIVINE. However, a migration to standalone package is in progress on github.

The Battle for Middle-earth: Reforged

As a fan, I help with the resurrection of an old realtime strategy (The Battle for the Middle-earth). I involve in the development of core game mechanics and engine programming. The project is written on a new unreal engine in C++. Find more about the project on project website.


A small tool that generates C++ monitors suited for LTL model cheking. It uses SPOT as an underlying library to generate an automata structure. (github)

Personal website of Henrich Lauko