Dominic Steinhöfel is a postdoctoral researcher of computer science at CISPA Helmholtz Center for Information Security, working in the research group of Andreas Zeller. His research interests center around program verification, including automated testing (mainly specification-based fuzzing) and program proving (mostly using symbolic execution).
Previously, he contributed Abstract Execution, a specification and verification framework for modeling and automatically proving conditional correctness of program transformations. His tool REFINITY, a workbench for modeling Java program transformations, has been used to extract preconditions for the safe application of code refactoring techniques. Currently, he is working on specifying and learning semantic constraints of system inputs for targeted fuzzing and program understanding.
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
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.