| HACL*: A verified modern cryptographic library JK Zinzindohoué, K Bhargavan, J Protzenko, B Beurdouche Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications …, 2017 | 371 | 2017 |
| Verified low-level programming embedded in F* J Protzenko, JK Zinzindohoué, A Rastogi, T Ramananandro, P Wang, ... Proc. {ACM} Program. Lang., 2017 | 210 | 2017 |
| Implementing and proving the TLS 1.3 record layer K Bhargavan, A Delignat-Lavaud, C Fournet, M Kohlweiss, J Pan, ... SP 2017-38th IEEE Symposium on Security and Privacy, 463-482, 2017 | 174* | 2017 |
| Evercrypt: A fast, verified, cross-platform cryptographic provider J Protzenko, B Parno, A Fromherz, C Hawblitzel, M Polubelova, ... 2020 IEEE Symposium on Security and Privacy (SP), 983-1002, 2020 | 159 | 2020 |
| Catala: a programming language for the law D Merigoux, N Chataing, J Protzenko Proceedings of the ACM on Programming Languages 5 (ICFP), 1-29, 2021 | 112 | 2021 |
| Everest: Towards a verified, drop-in replacement of HTTPS K Bhargavan, B Bond, A Delignat-Lavaud, C Fournet, C Hawblitzel, ... 2nd Summit on Advances in Programming Languages, 2017 | 109 | 2017 |
| {EverParse}: Verified secure {Zero-Copy} parsers for authenticated message formats T Ramananandro, A Delignat-Lavaud, C Fournet, N Swamy, T Chajed, ... 28th USENIX Security Symposium (USENIX Security 19), 1465-1482, 2019 | 101 | 2019 |
| Microsoft touch develop and the BBC micro: bit T Ball, J Protzenko, J Bishop, M Moskal, J De Halleux, M Braun, S Hodges, ... Proceedings of the 38th International Conference on Software Engineering …, 2016 | 98* | 2016 |
| Dijkstra monads for free D Ahman, C Hriţcu, K Maillard, G Martínez, G Plotkin, J Protzenko, ... Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming …, 2017 | 93 | 2017 |
| Aeneas: Rust verification by functional translation S Ho, J Protzenko Proceedings of the ACM on Programming Languages 6 (ICFP), 711-741, 2022 | 86 | 2022 |
| Global sequence protocol: A robust abstraction for replicated shared state S Burckhardt, D Leijen, J Protzenko, M Fähndrich 29th European Conference on Object-Oriented Programming (ECOOP 2015), 568-590, 2015 | 81 | 2015 |
| Formally verified cryptographic web applications in WebAssembly J Protzenko, B Beurdouche, D Merigoux, K Bhargavan | 71 | 2019 |
| Meta-f: Proof automation with smt, tactics, and metaprograms G Martínez, D Ahman, V Dumitrescu, N Giannarakis, C Hawblitzel, ... European Symposium on Programming, 30-59, 2019 | 71 | 2019 |
| Programming with permissions in Mezzo F Pottier, J Protzenko ACM SIGPLAN Notices 48 (9), 173-184, 2013 | 58 | 2013 |
| A security model and fully verified implementation for the IETF QUIC record layer A Delignat-Lavaud, C Fournet, B Parno, J Protzenko, T Ramananandro, ... 2021 IEEE Symposium on Security and Privacy (SP), 1162-1178, 2021 | 47 | 2021 |
| The design and formalization of Mezzo, a permission-based programming language T Balabonski, F Pottier, J Protzenko ACM Transactions on Programming Languages and Systems (TOPLAS) 38 (4), 1-94, 2016 | 43 | 2016 |
| Haclxn: Verified generic SIMD crypto (for all your favourite platforms) M Polubelova, K Bhargavan, J Protzenko, B Beurdouche, A Fromherz, ... Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications …, 2020 | 37 | 2020 |
| Noise: A library of verified high-performance secure channel protocol implementations S Ho, J Protzenko, A Bichhawat, K Bhargavan 2022 IEEE Symposium on Security and Privacy (SP), 107-124, 2022 | 36 | 2022 |
| {TreeSync}: authenticated group management for messaging layer security T Wallez, J Protzenko, B Beurdouche, K Bhargavan 32nd USENIX Security Symposium (USENIX Security 23), 1217-1233, 2023 | 34 | 2023 |
| A modern compiler for the french tax code D Merigoux, R Monat, J Protzenko Proceedings of the 30th ACM SIGPLAN International Conference on Compiler …, 2021 | 27 | 2021 |
Karthikeyan BhargavanCryspen and INRIAVerified email at inria.fr
