A Framework for the Analysis of Access Control Models for Interactive Mobile Devices. - Juan Manuel Crespo; Gustavo Betarte; Carlos Luna 001 (TYPES, 2008)

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)

Secure Multi-Execution through Static Program Transformation. - Gilles Barthe; Juan Manuel Crespo; Dominique Devriese; Frank Piessens; Exequiel Rivas (FMOODS/FORTE, 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)

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)

Mind the Gap: Modular Machine-checked Proofs of One-Round Key Exchange Protocols. - Gilles Barthe; Juan Manuel Crespo; Yassine Lakhnech; Benedikt Schmidt (IACR Cryptol. ePrint Arch., 2015)

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)

Automation and Modularity of Cryptographic Proofs in the Computational Model. - Juan Manuel Crespo (2016)