Postdoctoral researcher at
IMDEA-Software Research
in Madrid Spain.
Contact
|
Research Interests
My research interests lie in the areas of formal program verification and program transformations. More precisely, I 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. The main objective of this analysis is to show that it is possible to transfer evidence of program correctness from a source program to its compiled counterpart.
- Abstract Interpretation.
- Static Analysis.
- Semantics of Programming Languages.
- Formal Program Verification.
- Compilers, Optimizations, Program Transformation.
- Proof Carrying Code.
Software
I contribute in the development of the following tool:- EasyCrypt is an automated tool for elaborating security proofs of cryptographic systems from proof sketches---compact, formal representations of the essence of a proof as a sequence of games and hints. Proof sketches are checked automatically using off-the-shelf SMT solvers and automated theorem provers. The tool supports most common reasoning patterns and is significantly easier to use than its predecessors.
Awards
- Juan de la Cierva Fellowship (from Feb 2011). Micinn, Spain
Publications
-
An abstract model of certificate translation
TOPLAS - July 2011
-
A machine-checked framework for relational separation logic
SEFM 2011
-
Relational Verification Using Product Programs
FM 2011
-
A Functional Framework for Result Checking
FLOPS 2010
-
Perspectives in Certificate Translation.
TGC 2010.
-
Certificate Translation for the Verification of Concurrent Programs
TGC 2010.
-
Unleashing relational program logics
(draft)
-
An introduction to Certificate Translation [PDF]
LNCS chapter of the FOSAD2009 Tutorial Lectures. -
Certificate Translation for Optimizing Compilers [ACM Link].
ACM Transactions on Programming Languages and Systems (TOPLAS)
June 2009. -
PhD Thesis
- César Kunz
Program Compilation and Proof Transformation.
INRIA Sophia Antipolis - Méditerranée. February 2009. - Certified Reasoning in Memory Hierarchies [pdf]. Gilles Barthe and César Kunz and Jorge Sacchini. In Asian Programming Languages and Systems Symposium (APLAS) December 2008.
- Preservation of proof obligations for hybrid verification methods [pdf]. Gilles Barthe and César Kunz and David Picharde and Julián Samborski-Forlese. In Software Engineering and Formal Methods (SEFM) November 2008.
- Certificate translation for specification-preserving advices [pdf] [slides]. Gilles Barthe and César Kunz. In Foundations of Aspect-Oriented Languages (FOAL), 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), April 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), August 2006.