Dominic Steinhöfel

Postdoctoral Researcher in Computer Science

CISPA Helmholtz Center for Information Security

About me.

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.

Interests

Specification-Based Fuzzing
Specification Mining
Program Proving
Symbolic Execution
Formal Languages

Education

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

Affiliations

Postdoctoral Researcher

CISPA Helmholtz Center for Information Security

Jan 2021 – Present Saarbrücken, Germany

Research Assistant (Postdoctoral Researcher)

Technical University of Darmstadt

May 2020 – Dec 2020 Darmstadt, Germany

Research Assistant (Doctoral Researcher)

Technical University of Darmstadt

May 2015 – May 2020 Darmstadt, Germany

Projects

Last updated on Aug 7, 2020 tools

REFINITY

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.

Last updated on Aug 7, 2020

The KeY Project

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).

Featured Publications

Certified Abstract Cost Analysis

A program containing placeholders for unspecified statements or expressions is called an abstract (or schematic) program. Placeholder …

Elvira Albert, Reiner Hähnle, Alicia Merayo, Dominic Steinhöfel

Safer Parallelization

Adapting sequential legacy software to parallel environments can not only save time and money, but additionally avoids the loss of …

Reiner Hähnle, Asmae Heydari Tabar, Arya Mazaheri, Mohammad Norouzi, Dominic Steinhöfel, Felix Wolf

REFINITY to Model and Prove Program Transformation Rules

REFINITY is a workbench for modeling statement-level transformation rules on Java programs with the aim to formally verify their …

Dominic Steinhöfel

Abstract Execution: Automatically Proving Infinitely Many Programs

PhD thesis introducing a complete framework for Abstract Execution, as well a general framework for symbolic execution, model and …

Dominic Steinhöfel

Ever Change a Running System: Structured Software Reengineering Using Automatically Proven-Correct Transformation Rules

Legacy systems are business-critical software systems whose failure can have a significant impact on the business. Yet, their …

Dominic Steinhöfel

See all publications

Teaching

Own Courses

During my time at CISPA, I was the main organizer of several seminars held together with Andreas Zeller.

2022: Multimodal seminar on Symbolic Execution (upcoming)
This seminar focuses on central aspects of symbolic execution. It consists of lecture, paper presentation, and lab sessions. I developed all the concepts and technical materials of the lecture and lab parts.
2021/22: Seminar on Automated Testing and Debugging
This seminar covers fuzzing, property-based testing, specification inference, and debugging approaches like Delta and Statistical Debugging.
2021: Seminar on Specification and Testing
In this seminar, we discussed approaches to specification-based automated testing and mining specifications based on dynamic execution data.

Teaching Assistant

2016/17, 2017/18: Software Engineering Lecture
For this mandatory course for Bachelor students at TU Darmstadt, I organized the exercises, including tutor supervision, preparing exercise sheets, and chairing exercise sessions.
2015, 2015/16, 2017/18: Bachelor Lab
This is a mandatory course for Bachelor students at TU Darmstadt. Students work in teams on assigned software projects during a 6-month period. I handled many aspects of the course’s organization.
Seminars: I supervised students in several seminars at TU Darmstadt.