José Bacelar Almeida

49 papers A* 12A 3B 2C 2Misc 1Journal 23Unranked 5
YearRankTypeTitle / Venue / Authors
2025 A* conf
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt.
SP
José Bacelar Almeida, Gustavo Xavier Delerue Marinho Alves, Manuel Barbosa, Gilles Barthe, Luís Esquível, Vincent Hwang, Tiago Oliveira, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub
2025 J jnl
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Gustavo Xavier Delerue Marinho Alves, Manuel Barbosa, Gilles Barthe, Luís Esquível, Vincent Hwang, Tiago Oliveira, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub
2025 A* conf
Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Xavier Delerue Marinho Alves, João Diogo Duarte, Benjamin Grégoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2025 B conf
Leakage-Free Probabilistic Jasmin Programs.
CPP
José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh
2024 — conf
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt.
CRYPTO (2)
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, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
2024 J jnl
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt.
IACR Cryptol. ePrint Arch.
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, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
2023 J jnl
Formally verifying Kyber Episode IV: Implementation correctness.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
2023 J jnl
Formally verifying Kyber Part I: Implementation Correctness.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
2023 J jnl
Leakage-Free Probabilistic Jasmin Programs.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh
2022 B conf
Verified Password Generation from Password Composition Policies.
IFM
Miguel Grilo, João Campos, João F. Ferreira, José Bacelar Almeida, Alexandra Mendes
2021 A* conf
Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.
CCS
José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
2021 J jnl
Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Manuel L. Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira
2021 J jnl
Towards Formal Verification of Password Generation Algorithms used in Password Managers.
CoRR
Miguel Grilo, João F. Ferreira, José Bacelar Almeida
2020 Misc conf
Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification.
INDOCRYPT
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira
2020 A* conf
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.
SP
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
2019 A* conf
A Machine-Checked Proof of Security for AWS Key Management Service.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019 J jnl
A Machine-Checked Proof of Security for AWS Key Management Service.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019 J jnl
Machine-Checked Proofs for Cryptographic Standards.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
2019 A* conf
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.
CCS
José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
2019 J jnl
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.
CoRR
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
2018 A conf
Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks.
CSF
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2018 J jnl
Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2018 J jnl
Teaching how to program using automated assessment and functional glossy games (experience report).
Proc. ACM Program. Lang.
José Bacelar Almeida, Alcino Cunha, Nuno Macedo, Hugo Pacheco, José Proença
2017 A* conf
A Fast and Verified Software Stack for Secure Function Evaluation.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
2017 J jnl
A Fast and Verified Software Stack for Secure Function Evaluation.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
2017 A* conf
Jasmin: High-Assurance and High-Speed Cryptography.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub
2016 J jnl
A Tool-Chain for High-Assurance Cryptographic Software.
ERCIM News
José Bacelar Almeida, Manuel Barbosa, Hugo Pacheco, Vitor Pereira
2016 A* conf
Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC.
FSE
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2016 A* conf
Verifying Constant-Time Implementations.
USENIX Security Symposium
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi
2015 J jnl
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2014 J jnl
CAOVerif: An open-source deductive verification platform for cryptographic software implementations.
Sci. Comput. Program.
José Bacelar Almeida, Manuel Barbosa, Jean-Christophe Filliâtre, Jorge Sousa Pinto, Bárbara Vieira
2014 J jnl
Verified Implementations for Secure and Verifiable Computation.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub
2013 A* conf
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2013 J jnl
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2013 J jnl
Formal verification of side-channel countermeasures using self-composition.
Sci. Comput. Program.
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira
2012 J jnl
Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella-Béguelin
2012 A* conf
Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols.
CCS
José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella-Béguelin
2011 — book
Rigorous Software Development - An Introduction to Program Verification.
José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa
2010 A conf
A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols.
ESORICS
José Bacelar Almeida, Endre Bangerter, Manuel Barbosa, Stephan Krenn, Ahmad-Reza Sadeghi, Thomas Schneider
2010 J jnl
A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Endre Bangerter, Manuel Barbosa, Stephan Krenn, Ahmad-Reza Sadeghi, Thomas Schneider
2010 J jnl
Deductive verification of cryptographic software.
Innov. Syst. Softw. Eng.
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira
2010 C conf
Partial Derivative Automata Formalized in Coq.
CIAA
José Bacelar Almeida, Nelma Moreira, David Pereira, Simão Melo de Sousa
2009 — conf
Deductive Verification of Cryptographic Software.
NASA Formal Methods
Manuel Barbosa, José Bacelar Almeida, Jorge Sousa Pinto, Bárbara Vieira
2009 C conf
Verifying Cryptographic Software Correctness with Respect to Reference Implementations.
FMICS
José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira
2008 J jnl
Deriving Sorting Algorithms
CoRR
José Bacelar Almeida, Jorge Sousa Pinto
2007 — conf
A Tool for Programming with Interaction Nets.
RULE@RDP
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça
2007 — conf
Token-passing Nets for Functional Languages.
WRS@RDP
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça
2006 — conf
A Local Graph-rewriting System for Deciding Equality in Sum-product Theories.
TERMGRAPH@ETAPS
José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça
2004 A conf
Bounded Version Vectors.
DISC
José Bacelar Almeida, Paulo Sérgio Almeida, Carlos Baquero