Recent & Upcoming Talks

Ever Touch a Running System
Changing software without breaking it! How to use Abstract Execution and REFINITY to automatically prove properties of program transformation rules.
Dominic Steinhöfel
Last updated on May 31, 2021
Ever Touch a Running System
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 …
Last updated on Dec 2, 2020
PDF
REFINITY to Model and Prove Program Transformation Rules
Invited Talk: 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 …
Last updated on Oct 6, 2020
PDF
The Trace Modality
We propose the trace modality, a concept to uniformly express a wide range of program verification problems. To demonstrate its …
Dominic Steinhöfel, Reiner Hähnle
Last updated on Aug 5, 2020
The Trace Modality
Abstract Execution
We propose a new static software analysis principle called Abstract Execution, generalizing Symbolic Execution: While the latter …
Dominic Steinhöfel, Reiner Hähnle
Last updated on Aug 5, 2020
PDF
Abstract Execution