José Bacelar Almeida

According to our database1, José Bacelar Almeida authored at least 31 papers between 2004 and 2020.

Collaborative distances:



In proceedings 
PhD thesis 


Online presence:



The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.
Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification.
Proceedings of the Progress in Cryptology - INDOCRYPT 2020, 2020

A Machine-Checked Proof of Security for AWS Key Management Service.
IACR Cryptol. ePrint Arch., 2019

Machine-Checked Proofs for Cryptographic Standards.
IACR Cryptol. ePrint Arch., 2019

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

Teaching how to program using automated assessment and functional glossy games (experience report).
Proc. ACM Program. Lang., 2018

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks.
IACR Cryptol. ePrint Arch., 2018

Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages.
Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, 2018

A Fast and Verified Software Stack for Secure Function Evaluation.
IACR Cryptol. ePrint Arch., 2017

Jasmin: High-Assurance and High-Speed Cryptography.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

Formalization of the pumping lemma for context-free languages.
J. Formaliz. Reason., 2016

A Tool-Chain for High-Assurance Cryptographic Software.
ERCIM News, 2016

On the Formalization of Some Results of Context-Free Language Theory.
Proceedings of the Logic, Language, Information, and Computation, 2016

Verifying Constant-Time Implementations.
Proceedings of the 25th USENIX Security Symposium, 2016

Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC.
IACR Cryptol. ePrint Arch., 2015

Formalization of context-free language theory.
CoRR, 2015

CAOVerif: An open-source deductive verification platform for cryptographic software implementations.
Sci. Comput. Program., 2014

Verified Implementations for Secure and Verifiable Computation.
IACR Cryptol. ePrint Arch., 2014

Formal verification of side-channel countermeasures using self-composition.
Sci. Comput. Program., 2013

Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.
IACR Cryptol. ePrint Arch., 2013

Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols.
IACR Cryptol. ePrint Arch., 2012

Rigorous Software Development - An Introduction to Program Verification.
Undergraduate Topics in Computer Science, Springer, ISBN: 978-0-85729-018-2, 2011

Deductive verification of cryptographic software.
Innov. Syst. Softw. Eng., 2010

A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols.
IACR Cryptol. ePrint Arch., 2010

Partial Derivative Automata Formalized in Coq.
Proceedings of the Implementation and Application of Automata, 2010

Verifying Cryptographic Software Correctness with Respect to Reference Implementations.
Proceedings of the Formal Methods for Industrial Critical Systems, 2009

A Tool for Programming with Interaction Nets.
Electron. Notes Theor. Comput. Sci., 2008

Token-passing Nets for Functional Languages.
Electron. Notes Theor. Comput. Sci., 2008

Deriving Sorting Algorithms
CoRR, 2008

A Local Graph-rewriting System for Deciding Equality in Sum-product Theories.
Electron. Notes Theor. Comput. Sci., 2007

Bounded Version Vectors.
Proceedings of the Distributed Computing, 18th International Conference, 2004