César Kunz
César Kunz
Postdoctoral Researcher, IMDEA Software
Verified email at imdea.org
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
EasyCrypt: A Tutorial
G Barthe, F Dupressoir, B Grégoire, C Kunz, B Schmidt, PY Strub
Foundations of security analysis and design vii, 146-166, 2013
1162013
Verified computational differential privacy with applications to smart metering
G Barthe, G Danezis, B Grégoire, C Kunz, S Zanella-Beguelin
2013 IEEE 26th Computer Security Foundations Symposium, 287-301, 2013
672013
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
622013
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
Certificate translation for optimizing compilers
G Barthe, B Grégoire, C Kunz, T Rezk
International Static Analysis Symposium, 301-317, 2006
452006
Proving differential privacy in Hoare logic
G Barthe, M Gaboardi, EJG Arias, J Hsu, C Kunz, PY Strub
2014 IEEE 27th Computer Security Foundations Symposium, 411-424, 2014
432014
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
Verified security of merkle-damgård
M Backes, G Barthe, M Berg, B Grégoire, C Kunz, M Skoruppa, ...
2012 IEEE 25th Computer Security Foundations Symposium, 354-368, 2012
34*2012
Certificate translation in abstract interpretation
G Barthe, C Kunz
European Symposium on Programming, 368-382, 2008
282008
Certificate translation for optimizing compilers
G Barthe, B Grégoire, C Kunz, T Rezk
ACM Transactions on Programming Languages and Systems (TOPLAS) 31 (5), 1-45, 2009
242009
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
Preservation of proof pbligations for hybrid verification methods
G Barthe, C Kunz, D Pichardie, J Samborski-Forlese
2008 Sixth IEEE International Conference on Software Engineering and Formal …, 2008
112008
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
Certified reasoning in memory hierarchies
G Barthe, C Kunz, JL Sacchini
Asian Symposium on Programming Languages and Systems, 75-90, 2008
62008
EasyCrypt: Computer-Aided Cryptographic Proofs
G Barthe, F Dupressoir, B Gregoire, A Stoughton, PY Strub
42018
Automation in computer-aided cryptography: proofs, attacks and designs
G Barthe, B Grégoire, C Kunz, Y Lakhnech, SZ Béguelin
International Conference on Certified Programs and Proofs, 7-8, 2012
42012
Certificate translation for specification-preserving advices
G Barthe, C Kunz
Proceedings of the 7th workshop on Foundations of aspect-oriented languages …, 2008
42008
Automated analysis and synthesis of padding-based encryption schemes
G Barthe, S Zanella-Beguelin, JM Crespo, C Kunz, Y Lakhnech, ...
32012
The system can't perform the operation now. Try again later.
Articles 1–20