| A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification A Guéneau, A Charguéraud, F Pottier European Symposium on Programming, 533-560, 2018 | 58 | 2018 |
| Verified characteristic formulae for CakeML A Guéneau, MO Myreen, R Kumar, M Norrish Programming Languages and Systems: 26th European Symposium on Programming …, 2017 | 55 | 2017 |
| Efficient and provable local capability revocation using uninitialized capabilities AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, ... Proceedings of the ACM on Programming Languages 5 (POPL), 1-30, 2021 | 32 | 2021 |
| Formal proof and analysis of an incremental cycle detection algorithm A Guéneau, JH Jourdan, A Charguéraud, F Pottier Interactive Theorem Proving, 2019 | 30 | 2019 |
| Theorems for free from separation logic specifications L Birkedal, T Dinsdale-Young, A Guéneau, G Jaber, K Svendsen, ... Proceedings of the ACM on Programming Languages 5 (ICFP), 1-29, 2021 | 15 | 2021 |
| Proving full-system security properties under multiple attacker models on capability machines T Van Strydonck, AL Georges, A Guéneau, A Trieu, A Timany, F Piessens, ... 2022 IEEE 35th Computer Security Foundations Symposium (CSF), 80-95, 2022 | 8 | 2022 |
| Cerise: Program verification on a capability machine in the presence of untrusted code AL Georges*, A Guéneau*, T Van Strydonck, A Timany, A Trieu*, ... Journal of the ACM 71 (1), 1-59, 2024 | 7 | 2024 |
| Melocoton: A program logic for verified interoperability between ocaml and c A Guéneau, J Hostert, S Spies, M Sammler, L Birkedal, D Dreyer Proceedings of the ACM on Programming Languages 7 (OOPSLA2), 716-744, 2023 | 7 | 2023 |
| Mechanized Verification of the Correctness and Asymptotic Complexity of Programs A Guéneau Université de Paris, 2019 | 7 | 2019 |
| Mechanized Verification of the Correctness and Asymptotic Complexity of Programs.(Vérification mécanisée de la correction et complexité asymptotique de programmes). A Guéneau Inria, Paris, France, 2019 | 7 | 2019 |
| Cap’ou pas cap’?: Preuve de programmes pour une machine à capacités en présence de code inconnu AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, D Devriese, ... Journées Francophones des Langages Applicatifs 2021, 2021 | 6 | 2021 |
| Procrastination: A proof engineering technique A Guéneau Coq Workshop 2018, 2018 | 6 | 2018 |
| Thunks and Debits in Separation Logic with Time Credits F Pottier, A Guéneau, JH Jourdan, G Mével POPL 2024-51st ACM SIGPLAN Symposium on Principles of Programming Languages …, 2024 | 3 | 2024 |
| The ins and outs of iteration in Mezzo A Guéneau, F Pottier, J Protzenko arXiv preprint arXiv:1311.7256, 2013 | 3 | 2013 |
| Mechanized verification of the correctness and asymptotic complexity of programs: the right answer at the right time A Guéneau Université Paris Cité, 2019 | 2 | 2019 |
| The ins and outs of iteration in Mezzo. Higher-Order Programming and Effects (HOPE), 2013 A Guéneau, F Pottier, J Protzenko | 2 | 2013 |
| The Logical Essence of Well-Bracketed Control Flow A Timany, A Guéneau, L Birkedal Proceedings of the ACM on Programming Languages 8 (POPL), 575-603, 2024 | | 2024 |
| Theorems for Free from Separation Logic Specifications N Tzevelekos, G Jaber, L Birkedal, T DINSDALE-YOUNG, A GUÉNEAU, ... | | 2021 |
| Mechanized Program Verification on a Capability Machine in Presence of Untrusted Code AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, ... | | 2020 |
| Rapport de projet G Beaudoire, B Jonglez, F Mouhartem, P Pradic, A Guéneau, J Ledent, ... Projet 2014, 2013 | | 2013 |
