I am a research fellow at Clavis, the competence centre for information security of the Niederrhein University of Applied Sciences. Additionally, I am working in the IT department of the Lukashospital in Neuss, where I am concerned with IT security and digitalization of healthcare processes.
Formerly, I worked in the software engineering and programming languages department at the University of Düsseldorf, Germany. My research there was centered around symbolic model checking techniques for high-level languages. Development took place in the constraint solver and model checker ProB.
My recent publications can be found on the publication list, as well as on Google Scholar, dblp or Microsoft Academic. Furthermore, I maintain several plugins for the Atom editor which can be found in the package registry. Other software can be found on my GitHub profile.
PhD in Computer Science, 2017
M.Sc. in Computer Science, 2012
B.Sc. in Mathematics, 2012
B.Sc. in Computer Science, 2010
BMoth is a prototypical model checker for models written in classical B. Initially, BMoth was a student project intended to teach basics of model checking and how to implement explicit-state and symbolic model checking algorithms. In consequence, its focus lies on reusing existing libraries to reduce implementation effort. Nowadays, BMoth serves as a testbed for novel algorithms and implementation techniques.
ProB is an animator, constraint solver and model checker for the B-Method. It allows fully automatic animation of B specifications, and can be used to systematically check a specification for a wide range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation.
Schiefbahner Str. 64