IMDEA Software

Iniciativa IMDEA

Inicio > Personal

César Kunz

PhD - École des Mines de Paris (ENSMP), France

La información de esta página podría estar desactualizada debido a que César Kunz no es ya miembro del Instituto.

Antiguo Post-doctoral Researcher

César Kunz
Página web:

Short bio

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 counterpart.


I contribute in the development of the following tool:

Research Interests


[BibTeX Format](DBLP)

César Kunz also has a personally maintained website.

Intereses de Investigación

Interaction between compilation and verification condition generators, proof carrying code.