| Formally verifying Kyber JB Almeida, SA Olmos, M Barbosa, G Barthe, F Dupressoir, B Grégoire, ... | 14 | 2024 |
| Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt JB Almeida, SA Olmos, M Barbosa, G Barthe, F Dupressoir, B Grégoire, ... Cryptology ePrint Archive, 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, ... | | 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 |
