REFINITY to Model and Prove Program Transformation Rules

Summary

is a workbench for modeling statement-level transformation rules on 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 program prover. We describe the user interface and functionality of , and illustrate its capabilities along the application to proving conditional correctness of a code refactoring rule.