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.
Continue reading “Proving the Correctness of Program Transformations with Abstract Execution and REFINITY”