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.

Interests

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

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

 
 
 
 
 

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

Recent Posts

PhD Thesis Published

My PhD thesis “Abstract Execution: Automatically Proving Infinitely Many Programs” has been published and is available for download (open access). The abstract and possible errata found after publication are listed on a separate page.
Last updated on Aug 5, 2020 1 min read publication
PhD Thesis Published

Extract Inkscape Layers to PDF files for LaTeX Beamer Presentations

Presentation of a script for using Inkscape as an editor for animations in LaTeX presentations.
Last updated on Aug 5, 2020 5 min read tools

Projects

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.

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

Recent & Upcoming Talks

How to Prove the Correctness of Refactoring Rules

In this tutorial session colocated with the International Conference on integrated Formal Methods (iFM), I gave a 30-minutes talk …
Dec 2, 2019 — Dec 1, 2019 Bergen, Norway
PDF

The Trace Modality

We propose the trace modality, a concept to uniformly express a wide range of program verification problems. To demonstrate its …
Oct 9, 2019 — Porto, Portugal
Dominic Steinhöfel, Reiner Hähnle
The Trace Modality

Abstract Execution

We propose a new static software analysis principle called Abstract Execution, generalizing Symbolic Execution: While the latter …
Oct 7, 2019 2:40 PM — Oct 10, 2019 10:00 PM Porto, Portugal
Dominic Steinhöfel, Reiner Hähnle
PDF
Abstract Execution

Contact