I am a postdoctoral researcher of computer science at CISPA Helmholtz Center for Information Security, working in the research group of Andreas Zeller. My research focuses on languages, techniques, and tools for increasing confidence in the software correctness. To this end, I work on testing and program proving approaches and design specification languages for the unit and system level. As part of my research, I contributed Abstract Execution, an automatic verification framework mainly for unit-level program transformations, and ISLa, a language and solver for complex string constraints for the precise testing and analysis of software systems.
PhD in Computer Science, 2020
Technical University of Darmstadt
MSc in Computer Science, 2015
Technical University of Darmstadt
BSc in Computer Science, 2013
Technical University of Darmstadt
ISLearn mines input invariants expressed in the ISLa language that are associated to some program behavior (e.g., “input is accepted”). It is based on a catalog of abstract ISLa patterns that are instantiated and filtered. The resulting invariants are ranked according to their specificity and recall w.r.t. a set of provided or automatically produced input samples.
ISLa (Input Specification Language) is a specification language with a solver for context-sensitive string constraints. Strings are structured using a context-free grammar, and ISLa constraints are expressed in terms of grammar elements. The ISLa solver can report unsatisfiability for unsatisfiable constraints, and generate thousands of sample strings for satisfiable ones. Applications of ISLa include high-precision fuzz testing, debugging based on precise failure circumstances reports, and understanding of program behavior.
REFINITY is a workbench for modeling statement-based program transformation rules using abstract programs, based on Abstract Execution. It provides GUI support for creating models, and sends proof obligations to the KeY program prover to prove correctness of the transformation model. Once created proof certificates can be saved and validated.
The KeY framework is in its core a deduction-based program prover for Java. It is used for research and teaching, and supports functional verification, symbolic debugging, information-flow security, automatic test case generation and more. I have been massively contributing to KeY since 2015. Due to my implementation of Abstract Execution based on KeY, the system can now also prove universal second-order program properties (using abstract programs).
During my time at CISPA, I was the main organizer of several seminars held together with Andreas Zeller.