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 correctness. It is based on Abstract Execution, a verification framework for abstract programs with a high degree of proof automation, and interfaces to the KeY program prover. We describe user interface and functionality of REFINITY, and illustrate its capabilities along the application to proving conditional correctness of a code refactoring rule.

Proc. APLAS 2020

Accepted for publication and presentation at the conference at November 29th to December 3rd, 2020.