| 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 | 147 | 2015 |
| Verified low-level programming embedded in F* K Bhargavan, A Delignat-Lavaud, C Fournet, C Hritcu, J Protzenko, ... arXiv preprint arXiv:1703.00053, 2017 | 92 | 2017 |
| 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 | 61 | 2014 |
| Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method T Ramananandro Formal Aspects of Computing 20 (1), 21-39, 2008 | 50 | 2008 |
| 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 (SNAPL 2017), 2017 | 44 | 2017 |
| Formal verification of object layout for C++ multiple inheritance T Ramananandro, G Dos Reis, X Leroy ACM SIGPLAN Notices 46 (1), 67-80, 2011 | 25 | 2011 |
| 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 | 22 | 2016 |
| 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 | 19 | 2018 |
| 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 | 16* | 2018 |
| EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider. J Protzenko, B Parno, A Fromherz, C Hawblitzel, M Polubelova, ... IACR Cryptol. ePrint Arch. 2019, 757, 2019 | 15 | 2019 |
| 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 | 15 | 2015 |
| Light source device M Okamoto, M Nakayama, I Takaya US Patent 6,552,502, 2003 | 15 | 2003 |
| 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 | 12 | 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 | 11 | 2012 |
| 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 | 9 | 2019 |
| 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 | 5 | 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, ... IACR Cryptol. ePrint Arch. 2020, 114, 2020 | 3 | 2020 |
| The Mondex case study with Alloy T Ramananandro | 3 | 2006 |
| Mechanized Formal Semantics and Verified Compilation for C++ Objects T Ramananandro | 2 | 2012 |
| Meta-F*: Metaprogramming and tactics in an effectful program verifier G Martınez, D Ahman, V Dumitrescu, N Giannarakis, C Hawblitzel, ... European Symposium on Programming (ESOP), 2019 | 1 | 2019 |
