Dominic Steinhöfel

Dominic Steinhöfel

Postdoctoral Researcher in Computer Science

Technical University of Darmstadt

About me.

Dominic Steinhöfel is a postdoctoral researcher of computer science at Technical University of Darmstadt. His research interests center around (deductive) program verification, mostly using symbolic execution techniques.

His current focus is on Software Reengineering techniques, which aim to transform software to increase mainly non-functional properties like maintainability or performance. Among his early contributions to the field is 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. On the more theoretical side, he contributed Modal Trace Logic, a framework for formalizing, e.g., program evolution and bug fixing.

His goals are to develop methods for creating robust, reliable software, using lightweight (testing) as well as heavyweight (deductive verification) techniques. Dominic’s focus is on basic research in the border zone between theory and practice. He always strives for usable tool support, even for theory-heavy results. As a longterm goal, he aims to establish a holistic landscape of theories and tools for safe and secure Software Reengineering.


  • Software Reengineering
  • Program Transformations
  • Program Verification
  • Symbolic Execution


  • 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



Research Assistant (Postdoctoral Researcher)

Technical University of Darmstadt

May 2020 – Present Darmstadt, Germany

Research Assistant (Doctoral Researcher)

Technical University of Darmstadt

May 2015 – May 2020 Darmstadt, Germany



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