| Deep specifications and certified abstraction layers R Gu, J Koenig, T Ramananandro, Z Shao, X Wu, SC Weng, H Zhang, ... ACM SIGPLAN Notices 50 (1), 595-608, 2015 | 269 | 2015 |
| Verified low-level programming embedded in F J Protzenko, JK Zinzindohoué, A Rastogi, T Ramananandro, P Wang, ... Proceedings of the ACM on Programming Languages 1 (ICFP), 1-29, 2017 | 161 | 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 | 125 | 2020 |
| End-to-end verification of stack-space bounds for C programs Q Carbonneaux, J Hoffmann, T Ramananandro, Z Shao ACM SIGPLAN Notices 49 (6), 270-281, 2014 | 98 | 2014 |
| 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 | 97 | 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 | 81 | 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 | 56 | 2019 |
| Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method T Ramananandro Formal Aspects of Computing 20, 21-39, 2008 | 54 | 2008 |
| Certified concurrent abstraction layers R Gu, Z Shao, J Kim, X Wu, J Koenig, V Sjöberg, H Chen, D Costanzo, ... ACM SIGPLAN Notices 53 (4), 646-661, 2018 | 51 | 2018 |
| A unified coq framework for verifying c programs with floating-point computations T Ramananandro, P Mountcastle, B Meister, R Lethin Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 44 | 2016 |
| 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 | 33 | 2021 |
| Formal verification of object layout for C++ multiple inheritance T Ramananandro, G Dos Reis, X Leroy ACM SIGPLAN Notices 46 (1), 67-80, 2011 | 28 | 2011 |
| A compositional semantics for verified separate compilation and linking T Ramananandro, Z Shao, SC Weng, J Koenig, Y Fu Proceedings of the 2015 Conference on Certified Programs and Proofs, 3-14, 2015 | 27 | 2015 |
| Steel: proof-oriented programming in a dependently typed concurrent separation logic A Fromherz, A Rastogi, N Swamy, S Gibson, G Martínez, D Merigoux, ... Proceedings of the ACM on Programming Languages 5 (ICFP), 1-30, 2021 | 26 | 2021 |
| A monadic framework for relational verification: applied to information security, program equivalence, and optimizations N Grimm, K Maillard, C Fournet, C Hriţcu, M Maffei, J Protzenko, ... Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018 | 23 | 2018 |
| Hardening attack surfaces with formally proven binary format parsers N Swamy, T Ramananandro, A Rastogi, I Spiridonova, H Ni, D Malloy, ... Proceedings of the 43rd ACM SIGPLAN International Conference on Programming …, 2022 | 22 | 2022 |
| Systems and methods for efficient targeting MM Baskaran, T Henretty, A Johnson, A Konstantinidis, MH Langston, ... US Patent 10,466,349, 2019 | 20 | 2019 |
| A mechanized semantics for C++ object construction and destruction, with applications to resource management T Ramananandro, G Dos Reis, X Leroy ACM SIGPLAN Notices 47 (1), 521-532, 2012 | 20 | 2012 |
| Fastver: Making data integrity a commodity A Arasu, B Chandramouli, J Gehrke, E Ghosh, D Kossmann, J Protzenko, ... Proceedings of the 2021 International Conference on Management of Data, 89-101, 2021 | 16 | 2021 |
| Accelerated low-rank updates to tensor decompositions M Baskaran, MH Langston, T Ramananandro, D Bruns-Smith, T Henretty, ... 2016 IEEE High Performance Extreme Computing Conference (HPEC), 1-7, 2016 | 13 | 2016 |
