Juan Manuel Crespo
Juan Manuel Crespo
Volkswagen AG
Verified email at volkswagen.de - Homepage
Title
Cited by
Cited by
Year
Relational verification using product programs
G Barthe, JM Crespo, C Kunz
International Symposium on Formal Methods, 200-214, 2011
1862011
From relational verification to SIMD loop synthesis
G Barthe, JM Crespo, S Gulwani, C Kunz, M Marron
Proceedings of the 18th ACM SIGPLAN symposium on Principles and practice of …, 2013
612013
Beyond 2-safety: Asymmetric product programs for relational program verification
G Barthe, JM Crespo, C Kunz
International Symposium on Logical Foundations of Computer Science, 29-43, 2013
552013
Fully automated analysis of padding-based encryption in the computational model
G Barthe, JM Crespo, B Grégoire, C Kunz, Y Lakhnech, B Schmidt, ...
Proceedings of the 2013 ACM SIGSAC conference on Computer & communications …, 2013
452013
Secure multi-execution through static program transformation
G Barthe, JM Crespo, D Devriese, F Piessens, E Rivas
Formal Techniques for Distributed Systems, 186-202, 2012
392012
Product programs and relational program logics
G Barthe, JM Crespo, C Kunz
Journal of Logical and Algebraic Methods in Programming 85 (5), 847-859, 2016
362016
Computer-aided cryptographic proofs
G Barthe, JM Crespo, B Grégoire, C Kunz, SZ Béguelin
International Conference on Interactive Theorem Proving, 11-27, 2012
222012
Mind the gap: Modular machine-checked proofs of one-round key exchange protocols
G Barthe, JM Crespo, Y Lakhnech, B Schmidt
Annual International Conference on the Theory and Applications of …, 2015
212015
Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor
H Becker, JM Crespo, J Galowicz, U Hensel, Y Hirai, C Kunz, K Nakata, ...
International Symposium on Formal Methods, 69-84, 2016
82016
EasyCrypt: Computer-Aided Cryptographic Proofs
G Barthe, F Dupressoir, B Gregoire, A Stoughton, PY Strub
42018
Automated analysis and synthesis of padding-based encryption schemes
G Barthe, S Zanella-Beguelin, JM Crespo, C Kunz, Y Lakhnech, ...
32012
A machine-checked framework for relational separation logic
JM Crespo, C Kunz
International Conference on Software Engineering and Formal Methods, 122-137, 2011
32011
A certified access controller for jme-midp 2.0 enabled mobile devices
RR Oskui, G Betarte, C Luna
2009 International Conference of the Chilean Computer Science Society, 51-58, 2009
32009
A framework for the analysis of access control models for interactive mobile devices
JM Crespo, G Betarte, C Luna
International Workshop on Types for Proofs and Programs, 49-63, 2008
32008
Secure multi-execution through static program transformation: extended version
G Barthe, JM Crespo, D Devriese, F Piessens, E Rivas
CW Reports, 2012
22012
Unleashing relational program logics
G Barthe, J Crespo, C Kunz
Software. Imdea. Org, 1-17, 2010
12010
Automation and modularity of cryptographic proofs in the computational model
JM Crespo
Universidad Politécnica de Madrid, 2016
2016
Un Framework para el Análisis Formal de Modelos de Control de Acceso para Dispositivos Móviles Interactivos
JM Crespo
Facultad de Ciencias Exactas, Ingenieria y Agrimensura. Universidad Nacional …, 2009
2009
The EasyCrypt tool
G Barthe, B Grégoire, JM Crespo, C Kunz, S Zanella-Béguelin
Synthesis of Public-Key Encryption Schemes
G Barthe, JM Crespo, M Gagné, C Kunz, Y Lakhnech
The system can't perform the operation now. Try again later.
Articles 1–20