Invited Talk: How to Prove the Correctness of Refactoring Rules

Abstract

In this tutorial session colocated with the International Conference on integrated Formal Methods (iFM), I gave a 30-minutes talk presenting Abstract Execution and its application to proving program transformation rules. The participants used REFINITY in the second 30-minutes slot to prove the conditional correctness of two refactoring rules on their own.

Date
Dec 2, 2019 — Dec 1, 2019
Location
Bergen, Norway
Dominic Steinhöfel
Dominic Steinhöfel
Postdoctoral Researcher in Computer Science

My research interests include software reengineering, safe program transformation, program verification, and symbolic execution.