Work Proposal
The objective of the thesis is to focus on the interaction between compilation
and verification condition generators (VC generators), which are used in many interactive verification environments to guarantee the correctness of source programs, and by several proof carrying code (PCC) architectures to check the
correctness of compiled programs. Such VC generators operate on annotated
programs that carry loop invariants and procedure specifications expressed as
preconditions and postconditions, and yield a set of proof obligations that
must be discharged in order to establish the correctness of the program.
The main objective of the thesis is to show that it is possible to transfer
evidence of program correctness from a source program to its compiled
counterpart. The objective is to show, for an optimizing compiler, that one can
produce for every annotated program P :
 a function f that gives for every proof obligation at the
assembly level a corresponding proof obligation at the source level;
 a function that transforms, for every proof obligation p at the
assembly level, proofs of f(p) into proofs of p.
The work is carried in the context of the FET project MOBIUS.
Contact

Organization: 
INRIA 
Research Unit: 
Sophia Antipolis 
Project: 
Everest 
Phone: 
(+33/0) 4 97 15 53 44 
Fax: 
(+33/0) 4 92 38 50 29 
Email: 
Cesar dot Kunz at inria dot fr 

Research Interests
 Abstract Interpretation.
 Static Analysis.
 Semantics of Programming Languages.
 Formal Program Verification.
 Compilers, Optimizations, Program Transformation.
 Proof Carrying Code.
Publications
[
BibTeX Format]

Certified Reasoning in Memory Hierarchies
[pdf]
.
Gilles Barthe and César Kunz and Jorge Sacchini. In
Asian Programming Languages and Systems Symposium
(APLAS08) Bangalore, India, December 2008.

Preservation of proof obligations for hybrid verification methods
[pdf]
.
Gilles Barthe and César Kunz and David Picharde and Julián SamborskiForlese.
In
Software Engineering and Formal Methods
(SEFM08) Cape Town, South Africa, November 2008.

Certificate translation for specificationpreserving advices
[pdf]
[slides]
.
Gilles Barthe and César Kunz. In Foundations of AspectOriented
Languages (FOAL), Brussels, Belgium, April 2008.

Certificate Translation in Abstract Interpretation
[pdf]
[slides]..
Gilles Barthe and César Kunz. In Proceedings
of the 17th European Symposium on Programming (ESOP),
Budapest, Hungary, 2008.

Certificate Translation for Optimizing Compilers
[pdf].
Gilles Barthe, Benjamin Grégoire, César Kunz, and Tamara
Rezk. In Proceedings
of the 13th International Static Analysis Symposium (SAS),
Seoul, Korea, August 2006.