Jasmin: High-Assurance and High-Speed Cryptography. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Arthur Blot; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Hugo Pacheco 001; Benedikt Schmidt; Pierre-Yves Strub (CCS, 2017)

A Practical Framework for Privacy-Preserving NoSQL Databases. - Ricardo Macedo; João Paulo 001; Rogerio Pontes; Bernardo Portela; Tiago Oliveira 004; Miguel Matos; Rui Oliveira 001 (SRDS, 2017)

Are Deep Learning Methods Ready for Prime Time in Fingerprints Minutiae Extraction? - Ana Rebelo; Tiago Oliveira 004; Manuel Eduardo Correia; Jaime S. Cardoso 001 (CIARP, 2018)

BISEN: Efficient Boolean Searchable Symmetric Encryption with Verifiability and Minimal Leakage. - Guilherme Borges; Henrique João L. Domingos; Bernardo Ferreira; João Leitão 001; Tiago Oliveira 004; Bernardo Portela (IACR Cryptol. ePrint Arch., 2018)

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. - José Bacelar Almeida; Cécile Baritel-Ruet; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Alley Stoughton; Pierre-Yves Strub (CCS, 2019)

Machine-Checked Proofs for Cryptographic Standards. - José Bacelar Almeida; Cécile Baritel-Ruet; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Alley Stoughton; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2019)

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Vincent Laporte; Tiago Oliveira 004 (INDOCRYPT, 2020)

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Adrien Koutsos; Vincent Laporte; Tiago Oliveira 004; Pierre-Yves Strub (SP, 2020)

High-Assurance Cryptography Software in the Spectre Era. - Gilles Barthe; Sunjay Cauligi; Benjamin Grégoire; Adrien Koutsos; Kevin Liao; Tiago Oliveira 004; Swarn Priya; Tamara Rezk; Peter Schwabe (IACR Cryptol. ePrint Arch., 2020)

High-Assurance Cryptography in the Spectre Era. - Gilles Barthe; Sunjay Cauligi; Benjamin Grégoire; Adrien Koutsos; Kevin Liao; Tiago Oliveira 004; Swarn Priya; Tamara Rezk; Peter Schwabe (SP, 2021)

A Mobile Tele-Ophthalmology System for Planned and Opportunistic Screening of Diabetic Retinopathy in Primary Care. - Francisco Nunes; Pedro Madureira; Sílvia Rêgo; Cristiana Braga; Ruben Moutinho; Tiago Oliveira 004; Filipe Soares (IEEE Access, 2021)

Automated Adequacy Assessment of Cervical Cytology Samples Using Deep Learning. - Vladyslav Mosiichuk; Paula Viana; Tiago Oliveira 004; Luís Rosado (IbPRIA, 2022)

Impact of Generative Modeling for Fundus Image Augmentation With Improved and Degraded Quality in the Classification of Glaucoma. - Ricardo Leonardo; João Gonçalves; André V. Carreiro; Beatriz Simões; Tiago Oliveira 004; Filipe Soares (IEEE Access, 2022)

Typing High-Speed Cryptography against Spectre v1. - Basavesh Ammanaghatta Shivakumar; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Swarn Priya; Peter Schwabe; Lucas Tabary-Maujean (IACR Cryptol. ePrint Arch., 2022)

Boolean Searchable Symmetric Encryption With Filters on Trusted Hardware. - Bernardo Ferreira; Bernardo Portela; Tiago Oliveira 004; Guilherme Borges; Henrique João L. Domingos; João Leitão 001 (IEEE Trans. Dependable Secur. Comput., 2022)

High-speed and High-assurance Cryptographic Software - Tiago Oliveira 004 (2022)

Designing XAI-based Computer-aided Diagnostic Systems: Operationalising User Research Methods 25-36. - Elsa Oliveira; Cristiana Braga; Ana Sampaio; Tiago Oliveira 004; Filipe Soares; Luís Rosado (IUI Workshops, 2023)

Formally verifying Kyber Part I: Implementation Correctness. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2023)

Leakage-Free Probabilistic Jasmin Programs. - José Bacelar Almeida; Denis Firsov; Tiago Oliveira 004; Dominique Unruh (IACR Cryptol. ePrint Arch., 2023)

Schnorr protocol in Jasmin. - Denis Firsov; Tiago Oliveira 004; Dominique Unruh (IACR Cryptol. ePrint Arch., 2023)

Rethinking low-cost microscopy workflow: Image enhancement using deep based Extended Depth of Field methods. - Tomé Albuquerque; Luís Rosado; Ricardo P. M. Cruz; Maria João M. Vasconcelos; Tiago Oliveira 004; Jaime S. Cardoso 001 (Intell. Syst. Appl., 2023)

Formally verifying Kyber Episode IV: Implementation correctness. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre-Yves Strub (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023)

Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. - José Bacelar Almeida; Santiago Arranz-Olmos; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Cameron Low; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; et al. (IACR Cryptol. ePrint Arch., 2024)

Protecting cryptographic code against Spectre-RSB. - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (IACR Cryptol. ePrint Arch., 2024)

High-assurance zeroization. - Santiago Arranz-Olmos; Gilles Barthe; Ruben Gonzalez; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Peter Schwabe (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024)

Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants). - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (ASPLOS (2), 2025)

Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt. - José Bacelar Almeida; Gustavo Xavier Delerue Marinho Alves; Manuel Barbosa; Gilles Barthe; Luís Esquível; Vincent Hwang; Tiago Oliveira 004; Hugo Pacheco 001; Peter Schwabe; Pierre-Yves Strub (SP, 2025)

Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code. - Santiago Arranz-Olmos; Gilles Barthe; Benjamin Grégoire; Jan Jancar; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2025)

Protecting cryptographic code against Spectre-RSB. - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (Zenodo, 2025)

Protecting cryptographic code against Spectre-RSB. - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (Zenodo, 2025)