| Issue Date | Title | Author(s) |
| 2014 | CAOVerif: An open-source deductive verification platform for cryptographic software implementations | José Bacelar Almeida; Manuel Barbosa; Filliatre,JC; Jorge Sousa Pinto; Vieira,B |
| 2013 | Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations | José Bacelar Almeida; Manuel Barbosa; Barthe,G; Dupressoir,F |
| 2018 | Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks | Hugo Pereira Pacheco; Bernardo Luís Portela; Vítor Parreira Pereira; José Bacelar Almeida; Manuel Barbosa; Barthe,G; 5647; 5604; 5598; 6374; 6060 |
| 2017 | A Fast and Verified Software Stack for Secure Function Evaluation | José Bacelar Almeida; Manuel Barbosa; Barthe,G; Dupressoir,F; Grégoire,B; Laporte,V; Vítor Parreira Pereira |
| 2013 | Formal verification of side-channel countermeasures using self-composition | José Bacelar Almeida; Manuel Barbosa; Jorge Sousa Pinto; Vieira,B |
| 2016 | Formalization of the Pumping Lemma for Context-Free Languages | Ramos,MarcusViniciusMidena; Queiroz,RuyJ.G.B.de; Moreira,Nelma; José Bacelar Almeida |
| 2017 | Jasmin: High-Assurance and High-Speed Cryptography | José Bacelar Almeida; Manuel Barbosa; Barthe,G; Blot,A; Grégoire,B; Laporte,V; Oliveira,T; Hugo Pereira Pacheco; Schmidt,B; Strub,PY |
| 2019 | A Machine-Checked Proof of Security for AWS Key Management Service | José Bacelar Almeida; Tasiran,S; Strub,PY; Portela,B; Pereira,V; Gregoire,B; Cohen,E; Campagna,M; Barthe,G; Manuel Barbosa; 5604; 5598 |
| 2019 | Machine-Checked Proofs for Cryptographic Standards Indifferentiability of SPONGE and Secure High-Assurance Implementations of SHA-3 | José Bacelar Almeida; Strub,PY; Stoughton,A; Tiago Filipe Oliveira; Laporte,V; Gregoire,B; Dupressoir,F; Barthe,G; Manuel Barbosa; Baritel Ruet,C; 6207; 5598; 5604 |
| 2016 | On the Formalization of Some Results of Context-Free Language Theory | Midena Ramos,MVM; de Queiroz,RJGB; Moreira,N; José Bacelar Almeida |
| 2019 | Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages | José Bacelar Almeida; Ramos,MVM; Moreira,N; de Queiroz,RJGB; 5598 |
| 2016 | A Tool-Chain for High-Assurance Cryptographic Software | José Bacelar Almeida; Manuel Barbosa; Hugo Pereira Pacheco; Pereira,V |
| 2016 | Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC | José Bacelar Almeida; Manuel Barbosa; Barthe,G; Dupressoir,F |
| 2016 | Verifying Constant-Time Implementations | José Bacelar Almeida; Manuel Barbosa; Barthe,G; Dupressoir,F; Emmi,M |
