Properties preservation during transformation

• Author(s): Cruz, Daniela da ; Pinto, Jorge Sousa ; Henriques, Pedro Rangel
• Date: 2008
• Persistent ID: http://hdl.handle.net/1822/8106
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): Program verification and validation; Proof carrying code; Software analysis and transformation
• Document Type: Conference Object
• Language: English

Description

To prove the correctness of a program (written in a high level programming language) with respect to a specification (a set of proof obligations) does not assure the correctness of the machine code that the end-user will run after compilation and deployment phases. The code generated by the compiler should be verified again to guarantee that its correctness was preserved, and then that it can be executed in safety. In the context of a Ph.D. work in the area of software analysis and transformation, we are looking for a suitable approach to prove that the software properties (validated at source level) are kept during translation. In this position paper we introduce our architectural proposal, and discuss the platform and we are building for Java+JML on the top of Eclipse.