| Preservation of speculative constant-time by compilation S Arranz Olmos, G Barthe, L Blatter, B Grégoire, V Laporte Proceedings of the ACM on Programming Languages 9 (POPL), 1293-1325, 2025 | 3 | 2025 |
| 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 | 3 | 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 | 3 | 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 |
| Transparent Decompilation for Timing Side-Channel Analyses SA Olmos, G Barthe, L Blatter, S van der Wall, Z Zhang arXiv preprint arXiv:2501.04183, 2025 | | 2025 |
| Transparent Decompilation for Timing Side-Channel Analyses S Arranz Olmos, G Barthe, L Blatter, S van der Wall, Z Zhang arXiv e-prints, arXiv: 2501.04183, 2025 | | 2025 |
| Formally verifying Kyber–Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt J Bacelar Almeida, S Arranz Olmos, M Barbosa, M Quaresma, P Schwabe, ... Cham: Spriner, 2024 | | 2024 |
| High-assurance zeroization S Arranz Olmos, G Barthe, R Gonzalez, B Gregoire, V Laporte, ... | | 2024 |
| Formally verifying Kyber JB Almeida, SA Olmos, M Barbosa, G Barthe, F Dupressoir, B Grégoire, ... | | 2024 |
| Soporte para ARM en un compilador verificado SA 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 |
| Soporte para ARM en un compilador verificado S Arranz Olmos, MM Pagano | | |
