Bounded Version Vectors. - José Bacelar Almeida; Paulo Sérgio Almeida; Carlos Baquero (DISC, 2004)

A Local Graph-rewriting System for Deciding Equality in Sum-product Theories. - José Bacelar Almeida; Jorge Sousa Pinto; Miguel Vilaça (TERMGRAPH@ETAPS, 2006)

Token-passing Nets for Functional Languages. - José Bacelar Almeida; Jorge Sousa Pinto; Miguel Vilaça (WRS@RDP, 2007)

A Tool for Programming with Interaction Nets. - José Bacelar Almeida; Jorge Sousa Pinto; Miguel Vilaça (RULE@RDP, 2007)

Deriving Sorting Algorithms - José Bacelar Almeida; Jorge Sousa Pinto (CoRR, 2008)

Verifying Cryptographic Software Correctness with Respect to Reference Implementations. - José Bacelar Almeida; Manuel Barbosa; Jorge Sousa Pinto; Bárbara Vieira (FMICS, 2009)

Partial Derivative Automata Formalized in Coq. - José Bacelar Almeida; Nelma Moreira; David Pereira; Simão Melo de Sousa (CIAA, 2010)

A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols. - José Bacelar Almeida; Endre Bangerter; Manuel Barbosa; Stephan Krenn; Ahmad-Reza Sadeghi; Thomas Schneider 003 (IACR Cryptol. ePrint Arch., 2010)

Deductive verification of cryptographic software. - José Bacelar Almeida; Manuel Barbosa; Jorge Sousa Pinto; Bárbara Vieira (Innov. Syst. Softw. Eng., 2010)

Rigorous Software Development - An Introduction to Program Verification. - José Bacelar Almeida; Maria João Frade; Jorge Sousa Pinto; Simão Melo de Sousa (Springer, 2011)

Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. - José Bacelar Almeida; Manuel Barbosa; Endre Bangerter; Gilles Barthe; Stephan Krenn; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2012)

Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir (IACR Cryptol. ePrint Arch., 2013)

Formal verification of side-channel countermeasures using self-composition. - José Bacelar Almeida; Manuel Barbosa; Jorge Sousa Pinto; Bárbara Vieira (Sci. Comput. Program., 2013)

Verified Implementations for Secure and Verifiable Computation. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Guillaume Davy; François Dupressoir; Benjamin Grégoire; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2014)

CAOVerif: An open-source deductive verification platform for cryptographic software implementations. - José Bacelar Almeida; Manuel Barbosa; Jean-Christophe Filliâtre; Jorge Sousa Pinto; Bárbara Vieira (Sci. Comput. Program., 2014)

Formalization of context-free language theory. - Marcus V. M. Ramos; Ruy J. G. B. de Queiroz; Nelma Moreira; José Carlos Bacelar Almeida (CoRR, 2015)

Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir (IACR Cryptol. ePrint Arch., 2015)

Verifying Constant-Time Implementations. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir; Michael Emmi (USENIX Security Symposium, 2016)

On the Formalization of Some Results of Context-Free Language Theory. - Marcus Vinícius Midena Ramos; Ruy J. G. B. de Queiroz; Nelma Moreira; José Carlos Bacelar Almeida (WoLLIC, 2016)

A Tool-Chain for High-Assurance Cryptographic Software. - José Bacelar Almeida; Manuel Barbosa; Hugo Pacheco 001; Vitor Pereira 002 (ERCIM News, 2016)

Formalization of the pumping lemma for context-free languages. - Marcus Vinícius Midena Ramos; José Carlos Bacelar Almeida; Nelma Moreira; Ruy José Guerra Barretto de Queiroz (J. Formaliz. Reason., 2016)

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 Fast and Verified Software Stack for Secure Function Evaluation. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2017)

Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages. - Marcus V. M. Ramos; José Carlos Bacelar Almeida; Nelma Moreira; Ruy J. G. B. de Queiroz (LSFA, 2018)

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Hugo Pacheco 001; Vitor Pereira 002; Bernardo Portela (IACR Cryptol. ePrint Arch., 2018)

Teaching how to program using automated assessment and functional glossy games (experience report). - José Bacelar Almeida; Alcino Cunha; Nuno Macedo 001; Hugo Pacheco 001; José Proença (Proc. ACM Program. Lang., 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)

A Machine-Checked Proof of Security for AWS Key Management Service. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Matthew Campagna; Ernie Cohen; Benjamin Grégoire; Vitor Pereira 002; Bernardo Portela; Pierre-Yves Strub; Serdar Tasiran (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)

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. - José Carlos Bacelar Almeida; Manuel Barbosa; Karim Eldefrawy; Stéphane Graham-Lengrand; Hugo Pacheco 001; Vitor Pereira 002 (CoRR, 2021)

Towards Formal Verification of Password Generation Algorithms used in Password Managers. - Miguel Grilo; João F. Ferreira 001; José Bacelar Almeida (CoRR, 2021)

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. - José Bacelar Almeida; Manuel Barbosa; Manuel L. Correia; Karim Eldefrawy; Stéphane Graham-Lengrand; Hugo Pacheco 001; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2021)

Verified Password Generation from Password Composition Policies. - Miguel Grilo; João Campos; João F. Ferreira 001; José Bacelar Almeida; Alexandra Mendes (IFM, 2022)

A formal treatment of the role of verified compilers in secure computation. - José Carlos Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Hugo Pacheco 001; Vitor Pereira 002; Bernardo Portela (J. Log. Algebraic Methods Program., 2022)

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)

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)

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)