Jos Bacelar Almeida
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
17
Venues
9
Active years
2009–2025
Best venue rank
A*
Where they publish
Papers
17 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | CCS | Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Xavier Delerue Marinho Alves, Joo Diogo Duarte, Benjamin Grgoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang |
| 2025 | CPP | Leakage-Free Probabilistic Jasmin Programs. | Jos Bacelar Almeida, Denis Firsov, Tiago Oliveira, Dominique Unruh |
| 2025 | SP | 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, Lus Esquvel, Vincent Hwang, Tiago Oliveira, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub |
| 2024 | CRYPTO | 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, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Jean-Christophe Lchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub |
| 2022 | IFM | Verified Password Generation from Password Composition Policies. | Miguel Grilo, Joo Campos, Joo F. Ferreira, Jos Bacelar Almeida, Alexandra Mendes |
| 2021 | CCS | 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, Stphane Graham-Lengrand, Hugo Pacheco, Vitor Pereira |
| 2020 | INDOCRYPT | Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira |
| 2020 | SP | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grgoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub |
| 2019 | CCS | Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. | Jos Bacelar Almeida, Ccile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub |
| 2019 | CCS | A Machine-Checked Proof of Security for AWS Key Management Service. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grgoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran |
| 2017 | CCS | Jasmin: High-Assurance and High-Speed Cryptography. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub |
| 2017 | CCS | A Fast and Verified Software Stack for Secure Function Evaluation. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Vitor Pereira |
| 2016 | FSE | Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franois Dupressoir |
| 2013 | CCS | Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franois Dupressoir |
| 2012 | CCS | Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols. | Jos Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella-Bguelin |
| 2010 | ESORICS | 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 |
| 2009 | FMICS | Verifying Cryptographic Software Correctness with Respect to Reference Implementations. | Jos Bacelar Almeida, Manuel Barbosa, Jorge Sousa Pinto, Brbara Vieira |