Follow
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
2692011
Easycrypt: A tutorial
G Barthe, F Dupressoir, B Grégoire, C Kunz, B Schmidt, PY Strub
International School on Foundations of Security Analysis and Design, 146-166, 2012
1982012
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
992013
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
832013
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
782013
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
632014
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
532013
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
502016
Certificate translation for optimizing compilers
G Barthe, B Grégoire, C Kunz, T Rezk
International Static Analysis Symposium, 301-317, 2006
492006
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
47*2012
Certificate translation in abstract interpretation
G Barthe, C Kunz
European Symposium on Programming, 368-382, 2008
312008
Computer-aided cryptographic proofs
G Barthe, JM Crespo, B Grégoire, C Kunz, S Zanella Béguelin
International Conference on Interactive Theorem Proving, 11-27, 2012
252012
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
252009
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
122008
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, ...
FM 2016: Formal Methods: 21st International Symposium, Limassol, Cyprus …, 2016
112016
Certified reasoning in memory hierarchies
G Barthe, C Kunz, JL Sacchini
Asian Symposium on Programming Languages and Systems, 75-90, 2008
92008
Automation in computer-aided cryptography: Proofs, attacks and designs
G Barthe, B Grégoire, C Kunz, Y Lakhnech, S Zanella Béguelin
International Conference on Certified Programs and Proofs, 7-8, 2012
52012
Certificate translation for specification-preserving advices
G Barthe, C Kunz
Proceedings of the 7th workshop on Foundations of aspect-oriented languages …, 2008
52008
An abstract model of certificate translation
G Barthe, C Kunz
ACM Transactions on Programming Languages and Systems (TOPLAS) 33 (4), 1-46, 2011
42011
Implementing a direct method for certificate translation
G Barthe, B Grégoire, S Heraud, C Kunz, A Pacalet
International Conference on Formal Engineering Methods, 541-560, 2009
42009
The system can't perform the operation now. Try again later.
Articles 1–20