José Carlos Bacelar Ferreira Junqueira de Almeida


AuthID: R-000-85N

Confirmed Publications: 41



11
TITLE: Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification
AUTHORS: José Bacelar Almeida ; Manuel Barbosa ; Gilles Barthe ; Vincent Laporte; Tiago Oliveira ;
PUBLISHED: 2020, SOURCE: INDOCRYPT, VOLUME: 12578 LNCS
INDEXED IN: Scopus DBLP CrossRef: 2
IN MY: ORCID
12
TITLE: The Last Mile: High-Assurance and High-Speed Cryptographic Implementations
AUTHORS: Almeida, JB ; Barbosa, M ; Barthe, G ; Grégoire, B; Koutsos, A; Laporte, V; Oliveira, T ; Strub, PY;
PUBLISHED: 2020, SOURCE: 41st IEEE Symposium on Security and Privacy (SP) in 2020 IEEE SYMPOSIUM ON SECURITY AND PRIVACY (SP 2020), VOLUME: 2020-May
INDEXED IN: Scopus WOS DBLP CrossRef: 36
IN MY: ORCID
13
TITLE: A Machine-Checked Proof of Security for AWS Key Management Service
AUTHORS: Almeida, JB ; Barbosa, M ; Barthe, G ; Campagna, M; Cohen, E; Gregoire, B; Pereira, V; Portela, B ; Strub, PY; Tasiran, S;
PUBLISHED: 2019, SOURCE: ACM SIGSAC Conference on Computer and Communications Security (CCS) in PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19)
INDEXED IN: Scopus WOS DBLP CrossRef: 19
IN MY: ORCID
14
TITLE: Machine-Checked Proofs for Cryptographic Standards
AUTHORS: 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;
PUBLISHED: 2019, SOURCE: IACR Cryptol. ePrint Arch., VOLUME: 2019
INDEXED IN: DBLP
IN MY: ORCID
15
TITLE: Machine-Checked Proofs for Cryptographic Standards Indifferentiability of SPONGE and Secure High-Assurance Implementations of SHA-3. Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3
AUTHORS: Almeida, JB ; Baritel Ruet, C; Barbosa, M ; Barthe, G ; Dupressoir, F; Grégoire, B; Laporte, V; Oliveira, T ; Stoughton, A; Strub, PY;
PUBLISHED: 2019, SOURCE: ACM SIGSAC Conference on Computer and Communications Security (CCS) in PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19)
INDEXED IN: Scopus WOS DBLP CrossRef: 29
IN MY: ORCID
16
TITLE: Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages PDF
AUTHORS: Ramos, MVM; Almeida, JCB ; Moreira, N ; de Queiroz, RJGB;
PUBLISHED: 2019, SOURCE: 13th Workshop on Logical and Semantic Frameworks with Applications (LSFA) in ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, VOLUME: 344
INDEXED IN: Scopus WOS DBLP arXiv CrossRef
IN MY: ORCID
17
TITLE: hnforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
AUTHORS: Almeida, JB ; Barbosa, M ; Barthe, G ; Pacheco, H ; Pereira, V ; Portela, B ;
PUBLISHED: 2018, SOURCE: 31st IEEE Computer Security Foundations Symposium (CSF) held as part of the Federated Logic Conference (FLoC) in IEEE 31ST COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2018), VOLUME: 2018-July
INDEXED IN: Scopus WOS DBLP CrossRef: 9 Unpaywall
IN MY: ORCID
18
TITLE: Teaching How to Program using Automated Assessment and Functional Glossy Games (Experience Report)
AUTHORS: Almeida, JB ; Cunha, A ; Macedo, N ; Pacheco, H ; Proença, J ;
PUBLISHED: 2018, SOURCE: 23rd ACM SIGPLAN International Conference on Functional Programming (ICFP) in PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES, VOLUME: 2, ISSUE: ICFP
INDEXED IN: Scopus WOS DBLP CrossRef: 14
IN MY: ORCID
19
TITLE: A Fast and Verified Software Stack for Secure Function Evaluation
AUTHORS: Almeida, JB ; Barbosa, M ; Barthe, G ; Dupressoir, F; Grégoire, B; Laporte, V; Pereira, V ;
PUBLISHED: 2017, SOURCE: 24th ACM-SIGSAC Conference on Computer and Communications Security (ACM CCS) in CCS'17: PROCEEDINGS OF THE 2017 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY
INDEXED IN: Scopus WOS DBLP CrossRef: 21 Unpaywall
IN MY: ORCID
20
TITLE: Jasmin: High-Assurance and High-Speed Cryptography. High-Assurance and High-Speed Cryptography
AUTHORS: José Bacelar Almeida ; Manuel Barbosa ; Gilles Barthe ; Arthur Blot; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira ; Hugo Pacheco ; Benedikt Schmidt; Pierre Yves Strub;
PUBLISHED: 2017, SOURCE: 24th ACM-SIGSAC Conference on Computer and Communications Security (ACM CCS) in CCS'17: PROCEEDINGS OF THE 2017 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY
INDEXED IN: Scopus WOS DBLP CrossRef: 86
IN MY: ORCID
Page 2 of 5. Total results: 41.

footer slogan

Useful Links

Get Help

© 2026 CRACS & Inesc TEC - All Rights Reserved Privacy Policy | Terms of Service