Previously: Postdoctoral researcher at IMDEA Software Institute in Madrid, Spain.


Contact
Organization: IMDEA Software
Phone: (+34) 913 363 743
Fax: (+34) 913 365 018
E-mail: Cesar dot My_last_name at imdea dot org


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 to 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

  • Verified Computational Differential Privacy with Applications to Smart Metering.
    Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin.
    CSF 2013.
  • Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification.
    Gilles Barthe, Juan Manuel Crespo, César Kunz.
    LFCS 2013
  • From relational verification to SIMD loop synthesis.
    Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron.
    PPOPP 2013 (Best paper award):
  • Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs.
    Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin.
    CPP 2012
  • Verified Security of Merkle-Damgård.
    Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin.
    CSF 2012
  • Computer-Aided Cryptographic Proofs.
    Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin.
    ITP 2012
  • Automated Analysis and Synthesis of Padding-Based Encryption Schemes.
    Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin.
    IACR Cryptology ePrint Archive 2012
  • An Abstract Model of Certificate Translation. [PDF]
    Gilles Barthe, César Kunz
    ACM Trans. Program. Lang. Syst. - July 2011
  • Relational Verification Using Product Programs [PDF]
    Gilles Barthe, Juan Manuel Crespo, César Kunz
    FM 2011
  • A Machine-Checked Framework for Relational Separation Logic [PDF]
    Juan Manuel Crespo, César Kunz
    SEFM 2011
  • A Functional Framework for Result Checking [pdf]
    Gilles Barthe, Pablo Buiras, César Kunz
    FLOPS 2010
  • Perspectives in Certificate Translation. [pdf]
    Gilles Barthe, César Kunz
    TGC 2010.
  • Certificate Translation for the Verification of Concurrent Programs [pdf]
    César Kunz.
    TGC 2010.
  • An introduction to Certificate Translation [pdf]
    Gilles Barthe, César Kunz
    FOSAD 2008 Tutorial Lectures.
  • Certificate Translation for Optimizing Compilers [ACM Link]
    Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk
    ACM Transactions on Programming Languages and Systems (TOPLAS) - June 2009.
  • Program Compilation and Proof Transformation [pdf]
    César Kunz
    PhD Thesis - INRIA Sophia Antipolis-Méditerranée.
    February 2009.
  • Implementing a Direct Method for Certificate Translation
    Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet
    ICFEM 2009
  • Program Parallelization Using Synchronized Pipelining.
    Leonardo Scandolo, César Kunz, Manuel V. Hermenegildo
    LOPSTR 2009
  • Certified Reasoning in Memory Hierarchies [pdf]
    Gilles Barthe and César Kunz and Jorge Sacchini.
    Asian Programming Languages and Systems Symposium (APLAS) December 2008.
  • Certificate Translation in Abstract Interpretation [pdf]
    Gilles Barthe and César Kunz.
    European Symposium on Programming (ESOP), April 2008.
  • Certificate translation for specification-preserving advices [pdf]
    Gilles Barthe and César Kunz.
    Foundations of Aspect-Oriented Languages (FOAL), April 2008.
  • Preservation of Proof Obligations for Hybrid Verification Methods [pdf].
    Gilles Barthe and César Kunz and David Picharde and Julián Samborski-Forlese.
    Software Engineering and Formal Methods (SEFM) November 2008.
  • Certificate Translation for Optimizing Compilers [pdf]
    Gilles Barthe, Benjamin Grégoire, César Kunz, and Tamara Rezk.
    Static Analysis Symposium (SAS), August 2006.