Proving the Correctness of Program Transformations with Abstract Execution and REFINITY

Summary. Abstract Execution (AE) is a new program analysis technique for automatically proving second-order properties about programs. It is based on the symbolic execution of abstract programs with second-order symbolic stores. Abrupt completion is analyzed in separate SE branches. AE has been successfully applied to show that almost all statement-based Java refactoring techniques are unsound—unless constrained with suitable preconditions. Assuming these preconditions, we automatically proved the transformations correct. With REFINITY, there is now tool support for using AE for your own problems.

Continue reading “Proving the Correctness of Program Transformations with Abstract Execution and REFINITY”