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 | 38 | 2021 |
Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities AL Georges, A Trieu, L Birkedal Proceedings of the ACM on Programming Languages 6 (OOPSLA1), 1-30, 2022 | 20 | 2022 |
Iris-wasm: Robust and modular verification of webassembly programs X Rao, AL Georges, M Legoupil, C Watt, J Pichon-Pharabod, P Gardner, ... Proceedings of the ACM on Programming Languages 7 (PLDI), 1096-1120, 2023 | 16 | 2023 |
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 | 9 | 2024 |
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 | 9 | 2022 |
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 | 7 | 2021 |
Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly M Legoupil, J Rousseau, AL Georges, J Pichon-Pharabod, L Birkedal Proceedings of the ACM on Programming Languages 8 (OOPSLA2), 304-332, 2024 | 2 | 2024 |
SECOMP: Formally Secure Compilation of Compartmentalized C Programs J Thibault, R Blanco, D Lee, S Argo, A Azevedo de Amorim, AL Georges, ... Proceedings of the 2024 on ACM SIGSAC Conference on Computer and …, 2024 | 1 | 2024 |
Designing and Proving Robust Safety of Efficient Capability Machine Programs AL Georges Aarhus Universitet, 2023 | 1 | 2023 |
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic SF Vindum, AL Georges, L Birkedal Proceedings of the 14th ACM SIGPLAN International Conference on Certified …, 2025 | | 2025 |
Data Race Freedom à la Mode AL Georges, B Peters, L Elbeheiry, L White, S Dolan, RA Eisenberg, ... Proceedings of the ACM on Programming Languages 9 (POPL), 656-686, 2025 | | 2025 |
Proving capability safety in the presence of indirect sentries Technical report J Rousseau, AL Georges, J Pichon-Pharabod, D Devriese, L Birkedal | | 2024 |
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 |
Cap’ou pas cap’? AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, D Devriese, ... 32 ème Journées Francophones des Langages Applicatifs, 157, 0 | | |
Program verification on a capability machine in presence of untrusted code AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, ... | | |
Mechanized Reasoning about a Capability Machine AL Georges, A Trieu, L Birkedal | | |
Toward Complete Stack Safety for Capability Machines AL Georges, A Guéneau, A Trieu, L Birkedal | | |