Certified Reasoning in Memory Hierarchies. - Gilles Barthe; César Kunz; Jorge Luis Sacchini (APLAS, 2008)

Certificate Translation in Abstract Interpretation. - Gilles Barthe; César Kunz (ESOP, 2008)

Certificate translation for specification-preserving advices. - Gilles Barthe; César Kunz (FOAL, 2008)

An Introduction to Certificate Translation. - Gilles Barthe; César Kunz (FOSAD, 2008)

Preservation of Proof Pbligations for Hybrid Verification Methods. - Gilles Barthe; César Kunz; David Pichardie; Julián Samborski-Forlese (SEFM, 2008)

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)

Certificate translation for optimizing compilers. - Gilles Barthe; Benjamin Grégoire; César Kunz; Tamara Rezk (ACM Trans. Program. Lang. Syst., 2009)

A Functional Framework for Result Checking. - Gilles Barthe; Pablo Buiras; César Kunz (FLOPS, 2010)

Perspectives in Certificate Translation. - Gilles Barthe; César Kunz (TGC, 2010)

Certificate Translation for the Verification of Concurrent Programs. - César Kunz (TGC, 2010)

Relational Verification Using Product Programs. - Gilles Barthe; Juan Manuel Crespo; César Kunz (FM, 2011)

A Machine-Checked Framework for Relational Separation Logic. - Juan Manuel Crespo; César Kunz (SEFM, 2011)

An Abstract Model of Certificate Translation. - Gilles Barthe; César Kunz (ACM Trans. Program. Lang. Syst., 2011)

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 001; 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 Cryptol. ePrint Arch., 2012)

Fully automated analysis of padding-based encryption in the computational model. - Gilles Barthe; Juan Manuel Crespo; Benjamin Grégoire; César Kunz; Yassine Lakhnech; Benedikt Schmidt; Santiago Zanella-Béguelin (CCS, 2013)

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)

EasyCrypt: A Tutorial. - Gilles Barthe; François Dupressoir; Benjamin Grégoire; César Kunz; Benedikt Schmidt; Pierre-Yves Strub (FOSAD, 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)

Proving Differential Privacy in Hoare Logic. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; César Kunz; Pierre-Yves Strub (CSF, 2014)

Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor. - Hanno Becker; Juan Manuel Crespo; Jacek Galowicz; Ulrich Hensel; Yoichi Hirai; César Kunz; Keiko Nakata 001; Jorge Luis Sacchini; Hendrik Tews; Thomas Tuerk (FM, 2016)

Product programs and relational program logics. - Gilles Barthe; Juan Manuel Crespo; César Kunz (J. Log. Algebraic Methods Program., 2016)