I am a PhD student in the Everest team at INRIA Sophia-Antipolis. My advisor is Gilles Barthe. I am working also with Benjamin Gregoire.


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
E-mail: 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]