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. More recently, he has been looking into modeling and automatically proving conditional correctness of program transformations using Abstract Execution, a verification framework for schematic programs.

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.


  • Program Verification
  • Deductive Verification
  • Symbolic Execution
  • Verified Program Transformations


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