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.
||(+33/0) 4 97 15 53 44
||(+33/0) 4 92 38 50 29
||Cesar dot Kunz at inria dot fr
- Abstract Interpretation.
- Static Analysis.
- Semantics of Programming Languages.
- Formal Program Verification.
- Compilers, Optimizations, Program Transformation.
- Proof Carrying Code.
Certified Reasoning in Memory Hierarchies
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
Gilles Barthe and César Kunz and David Picharde and Julián Samborski-Forlese.
Software Engineering and Formal Methods
(SEFM08) Cape Town, South Africa, November 2008.
Certificate translation for specification-preserving advices
Gilles Barthe and César Kunz. In Foundations of Aspect-Oriented
Languages (FOAL), Brussels, Belgium, April 2008.
Certificate Translation in Abstract Interpretation
Gilles Barthe and César Kunz. In Proceedings
of the 17th European Symposium on Programming (ESOP),
Budapest, Hungary, 2008.
Certificate Translation for Optimizing Compilers
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.