PhD - École des Mines de Paris (ENSMP), France
The information in this page may be outdated, as César Kunz is no longer a member of the Institute.
Former Post-doctoral Researcher
César Kunz received a Computer Science degree from the National University of Córdoba (UNC), Argentina in 2004. He continued his studies at INRIA,France, funded by the FP6 FET integrated project ”MOBIUS: Mobility, Ubiquity and Security”, and received a Ph.D. from the Ecole des Mines de Paris (ENSMP), France in February, 2009. He joined the IMDEA Software Institute as a postdoctoral researcher in February 2009.
His research interests lie around formal program analysis and verification,abstract interpretation, and program transformation. His primary research activities are centered on the certification of program correctness, the verification of compiler optimizations, and the transformation of verification results in the presence of 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
I contribute in the development of the following tool:
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.
- 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), 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), November 2008.
Certificate translation for specification-preserving advices.
Gilles Barthe and César Kunz. In Foundations of Aspect-Oriented
Languages (FOAL), April 2008.
Certificate Translation in Abstract Interpretation.
Gilles Barthe and César Kunz. In Proceedings
of the 17th European Symposium on Programming (ESOP), 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), August 2006.
César Kunz also has a personally maintained
Interaction between compilation and verification condition generators, proof carrying code.