| Formally verifying Kyber JB Almeida, SA Olmos, M Barbosa, G Barthe, F Dupressoir, B Grégoire, ... | 18 | 2024 |
| Formally Verifying Kyber: Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt JB Almeida, S Arranz Olmos, M Barbosa, G Barthe, F Dupressoir, ... Annual International Cryptology Conference, 384-421, 2024 | 1 | 2024 |
| Protecting cryptographic code against Spectre-RSB (and, in fact, all known Spectre variants) SA Olmos, G Barthe, C Chuengsatiansup, B Grégoire, V Laporte, ... | 1 | 2024 |
| High-assurance zeroization S Arranz Olmos, G Barthe, R Gonzalez, B Gregoire, V Laporte, ... | | 2024 |
| Preservation of Speculative Constant-time by Compilation SA Olmos, G Barthe, L Blatter, B Grégoire, V Laporte Cryptology ePrint Archive, 2024 | | 2024 |
| High-assurance zeroization SA Olmos, G Barthe, R Gonzalez, B Grégoire, V Laporte, JC Léchenet, ... IACR Transactions on Cryptographic Hardware and Embedded Systems 2024 (1 …, 2024 | | 2024 |
| Soporte para ARM en un compilador verificado S Arranz Olmos | | 2022 |
| A formalisation of LEGv8 in Agda SA Olmos, M Fernández, M Steinberg, A Gadea, E Gunther, M Pagano Proceedings of the 24th Brazilian Symposium on Context-Oriented Programming …, 2020 | | 2020 |
