About

The following rows form a condensed CV. Although not every detail is provided, such as achievements and non-reviewed publications / talks, this should give a rough overview of what I've been doing so far.

While the verification of reactive systems and their software is my primary research interest, I'm also interested in all kinds of constraint satisfaction problems, classical AI and reverse engineering.

Since 2014
PhD candidate
Informatik 11 – Embedded Software, RWTH Aachen University

Working on formal verification of control software from the automation domain. I leverage SAT/SMT solving and abstract interpretation to develop techniques for proving a program's compliance with various specifications, synthesis of safe parameters and automated test generation.

2012 – 2014
MSc in Computer Science
Informatik 2 – Software Modeling and Verification, RWTH Aachen University

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.

2009 – 2012
BSc in Computer Science
Informatik 11 – Embedded Software, RWTH Aachen University

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.

1999 – 2008
Abitur
Märkisches Gymnasium Schwelm

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.

2018
Verification Technology, Systems & Applications
UniGR Summer School

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

2017
Logical Methods for Safety and Security of Software Systems
Marktoberdorf Summer School

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.

Since 2014
Research Associate
Informatik 11 – Embedded Software, RWTH Aachen University

Teaching and working on Arcade.PLC, a platform for verification of software for industrial controllers, featuring model checking procedures and static analyses. The work on this project involves abstracting the concrete program semantics to avoid exhaustive exploration of the program's state space, and formalising and exploiting peculiarities of both the properties of interest and the domain.

2014
Teaching Assistant
Informatik 2 – Theory of Hybrid Systems, RWTH Aachen University

Assisted students in “Data Structures and Algorithms”.

2013
Research Assistant
Informatik 2 – Software Modeling and Verification, RWTH Aachen University

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

2012
Research Assistant
Informatik 11 – Embedded Software, RWTH Aachen University

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

2011
Teaching Assistant
Lehr- und Forschungsgebiet Informatik 2 – Programming Languages and Verification, RWTH Aachen University

Assisted students in “Programming Concepts”.

2011
Teaching Assistant
Informatik 7 – Logic and Theory of Discrete Systems, RWTH Aachen University

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

2010
Teaching Assistant
Lehr- und Forschungsgebiet Informatik 2 – Programming Languages and Verification, RWTH Aachen University

Assisted students in “Programming Concepts”.

2008 – 2009
Compulsory Social Service
Evangelische Kirchengemeinde Düsseldorf-Eller, Düsseldorf
2005 – 2007
Certified Youth Leader
CVJM Schwelm e.V.

Joint lead of YMCA-based youth work.

2018
Viability of BDDs in Property Directed Reachability
Master's Thesis
2018
Abstraction Refinement in Incremental Cycle-bounded Model Checking
Master's Thesis
2017
A Unifying Formalism for PDR-based Software Verification
Master's Thesis
2016
Cycle-bounded Model Checking of Reactive Programs
Master's Thesis
2015
IC3-based Model Checking for PLC Programs
Master's Thesis
2015
Efficient Encoding of PLC Programs for nuXmv
Bachelor's Thesis
2015 – 2019
Formal and semi-formal Methods for Embedded Software (Seminar)
Informatik 11 – Embedded Software, RWTH Aachen University

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

2015 – 2019
Formal Methods for Logic Control Software (Lecture & Exercises)
Informatik 11 – Embedded Software, RWTH Aachen University

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.

DEDS 2020
Leveraging Horn Clause Solving for Compositional Verification of PLC Software
Dimitri Bohlender, Stefan Kowalewski
RE 2019
Explainability as a Non-Functional Requirement
Maximilian Alexander Köhl, Dimitri Bohlender, Kevin Baum, Markus Langer, Daniel Oster, Timo Speith
IFM 2018
Design and Verification of Restart-robust Industrial Control Software
Dimitri Bohlender, Stefan Kowalewski
WODES 2018
Compositional Verification of PLC Software using Horn Clauses and Mode Abstraction
Dimitri Bohlender, Stefan Kowalewski
SAC 2018
Cycle-bounded Model Checking of PLC Software via Dynamic Large-Block Encoding
Dimitri Bohlender, Daniel Hamm, Stefan Kowalewski
ETFA 2017
A Priori Test Coverage Estimation for Automated Production Systems: Using Generated Behavior Models for Coverage Calculation
Sebastian Ulewicz, Birgit Vogel-Heuser, Hendrik Simon, Dimitri Bohlender, Mathias Obster, Stefan Kowalewski
WODES 2016
Concolic Test Generation for PLC Programs using Coverage Metrics
Dimitri Bohlender, Hendrik Simon, Nico Friedrich, Stefan Kowalewski, Stefan Hauck-Stattelmann
MBMV 2016
Symbolic Verification of PLC Safety-Applications based on PLCopen Automata
Dimitri Bohlender, Hendrik Simon, Stefan Kowalewski
ISoLA 2014
A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models
Dimitri Bohlender, Harold Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, Thomas Noll
DCDS 2013
Boolean and Modular Abstractions for Programmable Logic Controllers
Sebastian Biallas, Dimitri Bohlender, Stefan Kowalewski