| Formal verification of a constant-time preserving C compiler G Barthe, S Blazy, B Grégoire, R Hutin, V Laporte, D Pichardie, A Trieu Proceedings of the ACM on Programming Languages 4 (POPL), 1-30, 2019 | 123 | 2019 |
| Verifying constant-time implementations by abstract interpretation S Blazy, D Pichardie, A Trieu Journal of Computer Security 27 (1), 137-163, 2019 | 71 | 2019 |
| 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 | 36 | 2021 |
| Formal verification of control-flow graph flattening S Blazy, A Trieu Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 25 | 2016 |
| 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 | 17 | 2022 |
| Verified translation validation of static analyses G Barthe, S Blazy, V Laporte, D Pichardie, A Trieu 2017 IEEE 30th Computer Security Foundations Symposium (CSF), 405-419, 2017 | 9 | 2017 |
| 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 | 8 | 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 | 8 | 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 |
| A generic framework to develop and verify security mechanisms at the microarchitectural level: application to control-flow integrity M Baty, P Wilke, G Hiet, A Fontaine, A Trieu 2023 IEEE 36th Computer Security Foundations Symposium (CSF), 372-387, 2023 | 3 | 2023 |
| Aide à la conception et vérification de spécifications formelles de protocoles cryptographiques A Trieu, ARA Chatalic, B Tessiau, LSS Kachanovich Univ. Rennes, Rennes, France, Tech. Rep 1, 2014 | 2 | 2014 |
| 33èmes journées francophones des langages applicatifs C Keller, T Bourke, S Blazy, F Bour, G Bury, S Dumbrava, D Gallois-Wong, ... | | 2022 |
| 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 |
| Verifying constant-time implementations in a verified compilation toolchain A Trieu Université de Rennes, 2018 | | 2018 |
| A Study on the Preservation of Cryptographic Constant-Time Security in the CompCert Compiler A Trieu | | 2018 |
| Semantic preservation of constant-time policies during compilation V Laporte, D Pichardie, A Trieu, S Blazy | | |
| Program verification on a capability machine in presence of untrusted code AL Georges, A Guéneau, T Van Strydonck, A Timany, A Trieu, ... | | |
| Toward Complete Stack Safety for Capability Machines AL Georges, A Guéneau, A Trieu, L Birkedal | | |
| 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 | | |
| Mechanized Reasoning about a Capability Machine AL Georges, A Trieu, L Birkedal | | |
Sandrine BlazyProfessor of Computer Science, University of RennesVerified email at irisa.fr
