REFINITY to Model and Prove Program Transformation Rules

Abstract

REFINITY is a workbench for modeling statement-level transformation rules on Java programs with the aim to formally verify their correctness. It is based on Abstract Execution, a verification framework for abstract programs with a high degree of proof automation, and interfaces with the KeY program prover. We describe the user interface and functionality of REFINITY, and illustrate its capabilities along the application to proving conditional correctness of a code refactoring rule.

Dominic Steinhöfel

Postdoctoral Researcher in Computer Science

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