Having convinced the company of the need to evolve the fundamental technology, which revolves around a proprietary Datalog DSL, I led the endeavour in a skunkworks-style R&D team created for this purpose. The work involved classic language design & implementation topics, such as the incremental replacement of misguided language concepts without breaking the existing huge code base, and tool development to automate the error-prone workflows of developers and consultants using the language.

I was part of the core team of developers responsible for expressing customer-independent, fundamental concepts of the business domain in a JVM-embedded, proprietary Datalog DSL. The resulting “model” contained the logic of WorkforcePlus, and I was recruited help managing its increasing complexity. My analysis uncovered concrete deficiencies and misapprehensions in the home-made logic programming paradigm as the root cause. Thus, my main responsibilities were (re-)engineering of the most problematic business domain concepts at that time, and the introduction of modelling language constructs needed to enable more principled modelling.

Taught formal methods and worked on Arcade.PLC, a platform for verification of software for industrial controllers, featuring model checking procedures and static analyses. The work on this project involved abstracting the concrete program semantics to avoid exhaustive exploration of the program’s state space, and formalising & exploiting peculiarities of both the properties of interest and the domain.

Assisted students in “Data Structures and Algorithms”.

Worked on the compiler for the SLIM language in the HASDEL research project with the European Space Agency.

Developed static analyses and visualisations of signal-flow in Matlab/Simulink in a research project with Daimler AG.

Assisted students in “Programming Concepts”.

Assisted students in “Formal Systems, Automata, Processes”.

Assisted students in “Programming Concepts”.

Joint lead of YMCA-based youth work.

Original title is “Erweiterung von Datalog um Berechnung von Rängen”

Taught scientific writing and giving a talk on the basis of recent publications in the formal methods community.

Proposed the lecture and was reponsible for its design and all related materials. The lecture covers state-of-the-art techniques in static analysis and model checking of logic control software.

During this time I worked on formal verification of control software from the automation domain and graduated summa cum laude. In my thesis “Symbolic Methods for Formal Verification of Industrial Control Software” I leverage SMT solving and abstract interpretation to develop fully-automated procedures for proving a program’s compliance with various specifications that are relevant or unique to this domain.

I picked electrical engineering as minor subject and graduated with distinction. My thesis “Accelerating Predicate Abstraction for Probabilistic Automata” proposes a fully symbolic approach to probabilistic reachability checking for Markov decision processes. The results are implemented in the Storm model checker.

My thesis “Modular and Boolean Abstraction of PLC-Programs” implements counterexample-guided abstraction refinement of procedures and control flow for PLC software model checking in the Arcade.PLC tool.

Being enthusiastic about game programming, and the school not teaching anything related to computers, I brought a voluntary course into being where I taught programming to like-minded.

Applied for this edition to learn about both deductive verification and what to look out for when implementing BMC for LLVM IR.

Attended the summer school for all things formal. I applied for this edition since it had a particularly strong lineup of lecturers in the domain of software verification.