[an error occurred while processing this directive]

Master Thesis

Type of project:
Master Thesis at Wuhan University - China, December 2009 - June 2010

Tang Mei

Proof transforming compilation for Separation logic

Supervising Assistant:
Martin Nordio


As the emerged threaten caused by unsafe execution of mobile code, Proof-Carrying Code (PCC) was adopted to establish "trust" between the code producer and consumer. In PCC, the code producer generates a formal proof automatically by Certifying compiler which indicates the code’s adherence to the security properties specified by the code consumer.

Proof- Transforming Compilers (PTC) is a similar approach to Certifying compiler in PCC, but take a source proof as input and produce the bytecode proof, and with interactive source code verification compared to Certifying compiler, more complex properties can be handled. In order to simplify the translation from source proof to the bytecode level, they presented a Hoare- style logic for bytecode similar with the source code logic, proof transformation was formalized and soundness result was proved in their works.

Separation logic is an extension to Hoare logic that permits reasoning about shared mutable heap structures, and it has been utilized to modular reasoning in object- oriented languages in many works. In order to automatically translate source code proof to bytecode logic by PTC, a separation logic for bytecode is needed. This project consists of the separation logic for bytecode, and the translation from source to bytecode level.