José Bacelar Almeida
José Bacelar Almeida
HASLab / INESC TEC, Universidade do Minho
Verified email at di.uminho.pt
Title
Cited by
Cited by
Year
Verifying constant-time implementations
JB Almeida, M Barbosa, G Barthe, F Dupressoir, M Emmi
25th {USENIX} Security Symposium ({USENIX} Security 16), 53-70, 2016
1752016
Jasmin: High-assurance and high-speed cryptography
JB Almeida, M Barbosa, G Barthe, A Blot, B Grégoire, V Laporte, ...
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications …, 2017
742017
Rigorous software development: an introduction to program verification
JB Almeida, MJ Frade, JS Pinto, SM De Sousa
Springer Science & Business Media, 2011
652011
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations
JB Almeida, M Barbosa, G Barthe, F Dupressoir
Proceedings of the 2013 ACM SIGSAC conference on Computer & communications …, 2013
612013
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC
JB Almeida, M Barbosa, G Barthe, F Dupressoir
International Conference on Fast Software Encryption, 163-184, 2016
532016
A certifying compiler for zero-knowledge proofs of knowledge based on σ-protocols
JB Almeida, E Bangerter, M Barbosa, S Krenn, AR Sadeghi, T Schneider
European Symposium on Research in Computer Security, 151-167, 2010
532010
Formal verification of side-channel countermeasures using self-composition
JB Almeida, M Barbosa, JS Pinto, B Vieira
Science of Computer Programming 78 (7), 796-812, 2013
482013
Bounded version vectors
JB Almeida, PS Almeida, C Baquero
International Symposium on Distributed Computing, 102-116, 2004
432004
Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols
J Bacelar Almeida, M Barbosa, E Bangerter, G Barthe, S Krenn, ...
Proceedings of the 2012 ACM conference on Computer and communications …, 2012
382012
An overview of formal methods tools and techniques
JB Almeida, MJ Frade, JS Pinto, SM de Sousa
Rigorous Software Development, 15-44, 2011
372011
Partial Derivative Automata Formalized in Coq
JB Almeida, N Moreira, D Pereira, SM de Sousa
International Conference on Implementation and Application of Automata, 59-68, 2010
272010
A fast and verified software stack for secure function evaluation
JB Almeida, M Barbosa, G Barthe, F Dupressoir, B Grégoire, V Laporte, ...
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications …, 2017
222017
The last mile: high-assurance and high-speed cryptographic implementations
JB Almeida, M Barbosa, G Barthe, B Grégoire, A Koutsos, V Laporte, ...
2020 IEEE Symposium on Security and Privacy (SP), 965-982, 2020
192020
Deductive verification of cryptographic software
JB Almeida, M Barbosa, JS Pinto, B Vieira
Innovations in Systems and Software Engineering 6 (3), 203-218, 2010
172010
A tool for programming with interaction nets
JB Almeida, JS Pinto, M Vilaça
Electronic Notes in Theoretical Computer Science 219, 83-96, 2008
152008
Machine-checked proofs for cryptographic standards: Indifferentiability of sponge and secure high-assurance implementations of SHA-3
JB Almeida, C Baritel-Ruet, M Barbosa, G Barthe, F Dupressoir, ...
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications …, 2019
142019
Verifying cryptographic software correctness with respect to reference implementations
JB Almeida, M Barbosa, JS Pinto, B Vieira
International Workshop on Formal Methods for Industrial Critical Systems, 37-52, 2009
132009
A machine-checked proof of security for AWS key management service
JB Almeida, M Barbosa, G Barthe, M Campagna, E Cohen, B Gregoire, ...
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications …, 2019
82019
ON LINE-METAL COATING OF OPTICAL FIBRES
JB Almeida
81979
Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
JB Almeida, M Barbosa, G Barthe, H Pacheco, V Pereira, B Portela
2018 IEEE 31st Computer Security Foundations Symposium (CSF), 132-146, 2018
72018
The system can't perform the operation now. Try again later.
Articles 1–20