The following is a non-exhaustive list of projects I’ve been involved in, or still am, to varying degrees. Some of them are work-related, while others are just personal side projects, but all of them are interesting in their own way.
I was curious to explore what ClojureScript and Reagent are all about and used this opportunity to create a web frontend for the SAT-based Mastermind solver from one of my posts.
All computation is kept client-side to avoid server costs. I had to port the approach to C/C++ and kissat to obtain a reasonably small and performant WASM library. Ultimately, this library is what the thin ClojureScript frontend wraps.
With the end of my PhD looming on the horizon, I wanted to get a short CV and some information about me online. However, I wasn’t interested in generic, impersonal solutions, such as the services of career-oriented social networking sites.
I used this opportunity to learn some web development basics, and build a static website that serves as both a portfolio and an outlet for all things creative. It’s the site you’re looking at right now.
I worked on Arcade.PLC on two occasions: during my bachelor’s thesis, and my time as research associate at Embedded Software. Arcade.PLC is both a tool and a framework for formal verification of industrial control software, featuring procedures for static analysis, automated test generation and model checking.
It started out as explicit state-space exploration based on abstract interpretation, which is what I’ve been integrating abstractions into during my bachelor’s thesis, but was extended with various SMT-based methods during my PhD. In contrast to general purpose verifier backends, it is tailored to aid in the analysis of issues specific to the domain of industrial control. For some properties, like the analysis of restart-behaviour, it even is the only tool in existence.
I was involved in parsing & compiling source code to intermediate representations, and all parts of the verification pipeline:
Although SMT-LIB is the standard language supported by most SMT solvers, some of them introduce custom language extensions. Such extensions may range from syntactical sugar to fine-grained control over the underlying solver-procedure.
Since I’m an avid user of Z3, I started vim-smt2 to have a plugin for the Vim editor that supports both the base SMT-LIB language and the extensions provided by Z3. Besides the basic syntax highlighting I’m implementing convenient features, such as querying satisfiability or the solver’s version, when I find myself repeatedly doing automatable tasks manually.
In the context of my master’s thesis I’ve worked on the Storm probabilistic model checker. In particular, I developed a fully symbolic variant of the partially explicit procedure used in PASS for probabilistic reachability checking of Markov decision processes.
I used SMT-solving to compute a menu-based abstraction, and refine it in a counterexample-guided fashion. The abstraction was stored in terms of MTBDDs, for which I developed both the actual symbolic value iteration and symbolic static analyses for preprocessing.
When I was a research assistant at MOVES, I was involved in the HASDEL project. This was an ESA project, aiming to provide RAMS analyses tailored to the specific needs of launcher systems. Since this was a successor of the COMPASS project, the original COMPASS toolset had to be extended.
In COMPASS, the system specification is written in the SLIM language. I was mainly responsible for adapting the SLIM compiler front and middle end, to support the language extensions proposed for HASDEL. In line with this, I also handled arising change requests concerning the GUI, and automated the creation of a minimal Linux image for showcasing HASDEL.
When I was a research assistant at Embedded Software, I was involved in a research project with Daimler AG. With MATLAB Simulink being a popular choice for the development of embedded software in the automotive domain, this project aimed to develop model-based analyses to aid developers of Simulink models.
Tracking a signal’s (potential) flow manually, given the highly modular and hierarchical models, is prone to error. To simplify this, I adapted standard dataflow analyses for programs to this domain. I was also responsible for visualising results of such analyses in both Simulink and external frameworks.