Verifying constant-time implementations JB Almeida, M Barbosa, G Barthe, F Dupressoir, M Emmi 25th {USENIX} Security Symposium ({USENIX} Security 16), 53-70, 2016 | 166 | 2016 |
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 | 70 | 2017 |
Rigorous software development: an introduction to program verification JB Almeida, MJ Frade, JS Pinto, SM De Sousa Springer Science & Business Media, 2011 | 65 | 2011 |
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 | 60 | 2013 |
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 | 53 | 2010 |
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 | 52 | 2016 |
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 | 47 | 2013 |
Bounded version vectors JB Almeida, PS Almeida, C Baquero International Symposium on Distributed Computing, 102-116, 2004 | 43 | 2004 |
An overview of formal methods tools and techniques JB Almeida, MJ Frade, JS Pinto, SM de Sousa Rigorous Software Development, 15-44, 2011 | 37 | 2011 |
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 | 36 | 2012 |
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 | 27 | 2010 |
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 | 21 | 2017 |
Deductive verification of cryptographic software JB Almeida, M Barbosa, JS Pinto, B Vieira Innovations in Systems and Software Engineering 6 (3), 203-218, 2010 | 17 | 2010 |
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 | 16 | 2020 |
A tool for programming with interaction nets JB Almeida, JS Pinto, M Vilaça Electronic Notes in Theoretical Computer Science 219, 83-96, 2008 | 15 | 2008 |
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 | 13 | 2009 |
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 | 12 | 2019 |
ON LINE-METAL COATING OF OPTICAL FIBRES JB Almeida | 8 | 1979 |
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 | 6 | 2019 |
CAOVerif: An open-source deductive verification platform for cryptographic software implementations JB Almeida, M Barbosa, JC Filliâtre, JS Pinto, B Vieira Science of Computer Programming 91, 216-233, 2014 | 6 | 2014 |