José Bacelar Almeida

According to our database, José Bacelar Almeida authored at least 43 papers between 2004 and 2025.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2025

CCS25 - Artifact for "Jazzline: Composable CryptoLine functional correctness proofs for Jasmin programs".

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, João Diogo Duarte, Gustavo Xavier Delerue Marinho Alves, Benjamin Grégoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

Dataset, July, 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, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub

Proceedings of the IEEE Symposium on Security and Privacy, 2025

Leakage-Free Probabilistic Jasmin Programs.

José Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh

Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2025

Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs.

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

Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, 2025

2024

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, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub

Proceedings of the Advances in Cryptology - CRYPTO 2024, 2024

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, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub

IACR Trans. Cryptogr. Hardw. Embed. Syst., 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, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 2023

2022

A formal treatment of the role of verified compilers in secure computation.

José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela

J. Log. Algebraic Methods Program., 2022

Verified Password Generation from Password Composition Policies.

Miguel Grilo, João Campos, João F. Ferreira, José Bacelar Almeida, Alexandra Mendes

Proceedings of the Integrated Formal Methods - 17th International Conference, 2022

2021

Towards Formal Verification of Password Generation Algorithms used in Password Managers.

Miguel Grilo, João F. Ferreira, José Bacelar Almeida

CoRR, 2021

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, Vitor Pereira

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, Vitor Pereira

Proceedings of the CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15, 2021

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, Pierre-Yves Strub

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira

Proceedings of the Progress in Cryptology - INDOCRYPT 2020, 2020

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, 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, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

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, Alley Stoughton, Pierre-Yves Strub

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2018

Teaching how to program using automated assessment and functional glossy games (experience report).

José Bacelar Almeida, Alcino Cunha, Nuno Macedo, Hugo Pacheco, José Proença

Proc. ACM Program. Lang., 2018

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

Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, 2018

Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

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

Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

Jasmin: High-Assurance and High-Speed Cryptography.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub

Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

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

A Tool-Chain for High-Assurance Cryptographic Software.

José Bacelar Almeida, Manuel Barbosa, Hugo Pacheco, Vitor Pereira

ERCIM News, 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

Proceedings of the Logic, Language, Information, and Computation, 2016

Verifying Constant-Time Implementations.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi

Proceedings of the 25th USENIX Security Symposium, 2016

Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir

Proceedings of the Fast Software Encryption - 23rd International Conference, 2016

2015

Formalization of context-free language theory.

Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, José Carlos Bacelar Almeida

CoRR, 2015

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

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

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

Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir

Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

2012

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

Proceedings of the ACM Conference on Computer and Communications Security, 2012

2011

Rigorous Software Development - An Introduction to Program Verification.

José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, Simão Melo de Sousa

Undergraduate Topics in Computer Science, Springer, ISBN: 978-0-85729-018-2, 2011

2010

Partial Derivative Automata Formalized in Coq.

José Bacelar Almeida, Nelma Moreira, David Pereira, Simão Melo de Sousa

Proceedings of the Implementation and Application of Automata, 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

Proceedings of the Computer Security, 2010

2009

Deductive Verification of Cryptographic Software.

Manuel Barbosa, José Bacelar Almeida, Jorge Sousa Pinto, Bárbara Vieira

Proceedings of the First NASA Formal Methods Symposium, 2009

Verifying Cryptographic Software Correctness with Respect to Reference Implementations.

José Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Bárbara Vieira

Proceedings of the Formal Methods for Industrial Critical Systems, 2009

2008

Deriving Sorting Algorithms

José Bacelar Almeida, Jorge Sousa Pinto

CoRR, 2008

2007

A Tool for Programming with Interaction Nets.

José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça

Proceedings of the Eighth International Workshop on Rule Based Programming, 2007

Token-passing Nets for Functional Languages.

José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça

Proceedings of the 7th International Workshop on Reduction Strategies in Rewriting and Programming, 2007

2006

A Local Graph-rewriting System for Deciding Equality in Sum-product Theories.

José Bacelar Almeida, Jorge Sousa Pinto, Miguel Vilaça

Proceedings of the Third International Workshop on Term Graph Rewriting, 2006

2004

Bounded Version Vectors.

José Bacelar Almeida, Paulo Sérgio Almeida, Carlos Baquero

Proceedings of the Distributed Computing, 18th International Conference, 2004