José Bacelar Almeida

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

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2020
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

2019
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

2018
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

2017
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

2016
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

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

Formalization of context-free language theory.
CoRR, 2015

2014
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

2013
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

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

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

2010
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

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

2008
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

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

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


  Loading...