???global.info.a_carregar???
José Carlos Bacelar Almeida. Concluiu o(a) Doutoramento em Doutoramento em Informática em 2003 pelo(a) Universidade do Minho Escola de Engenharia, Doutoramento em Informática em 2003/06/20 pelo(a) Universidade do Minho, Mestrado em Mestrado em Informática em 1994 pelo(a) Universidade do Minho e Licenciatura em Engenharia Electrotécnica e de Computadores em 1991 pelo(a) Universidade do Porto Faculdade de Engenharia. É Professor Auxiliar no(a) Universidade do Minho, Professor Auxiliar no(a) Universidade do Minho e Investigador principal (carreira) no(a) Instituto de Engenharia de Sistemas e Computadores Tecnologia e Ciência Center for Research in Advanced Computing Systems. Publicou 19 artigos em revistas especializadas. Possui 1 livro(s). Coorientou 3 tese(s) de doutoramento. Orientou 27 dissertação(ões) de mestrado e coorientou 11. Recebeu 2 prémio(s) e/ou homenagens. Participa e/ou participou como Investigador em 6 projeto(s). Atua na(s) área(s) de Ciências Exatas com ênfase em Ciências da Computação e da Informação com ênfase em Ciências da Computação. No seu currículo Ciência Vitae os termos mais frequentes na contextualização da produção científica, tecnológica e artístico-cultural são: Runtime Verification; Formal Software Verification; Real-Time Embedded Systems; Cyber-Security; Nanotechnologies; Computer Engineering; Electrical and Computer Engineering - Computer Systems (Hardware/Software); Cryptography; Proof Assistants; verificação formal; segurança de passwords; segurança usável; verificação de implementações criptográficas; Verificação em Tempo de Execução; Verificação Formal de Software; Sistemas Embebidos de Tempo-Real; Segurança Informática; Segurança; Memória Não Volátil; Phase Change Memory; Criptografia; Sistema Embebidos; Verificação Formal e Proof Carrying Code; Sistema de Tipos e Analise Estáticas de Programas ; Desenho de Linguagens e Compilação; .
Ler resumo completo ↓
Identificação

Identificação pessoal

Nome completo
José Carlos Bacelar Almeida

Nomes de citação

  • Almeida, José Bacelar

Identificadores de autor

Ciência ID
4D17-69F5-2C51
ORCID iD
0000-0003-0011-7455
Google Scholar ID
José Bacelar Almeida
Researcher Id
I-8105-2015
Scopus Author Id
35316920400

Domínios de atuação

  • Ciências Exatas - Ciências da Computação e da Informação - Ciências da Computação

Idiomas

Idioma Conversação Leitura Escrita Compreensão Peer-review
Inglês Utilizador independente (B1) Utilizador proficiente (C1) Utilizador independente (B1) Utilizador independente (B1)
Francês Utilizador elementar (A1) Utilizador independente (B1) Utilizador elementar (A1) Utilizador elementar (A1)
Espanhol; Castelhano Utilizador elementar (A1) Utilizador elementar (A1) Utilizador elementar (A1) Utilizador elementar (A1)
Formação
Grau Classificação
2003
Concluído
 Doutoramento em Informática (Doutoramento)
Universidade do Minho Escola de Engenharia, Portugal
"Uma Abordagem à Verificação Automática de Protocolos Criptográficos" (TESE/DISSERTAÇÃO)
 Aprovado
1994
Concluído
 Mestrado em Informática (Mestrado)
Universidade do Minho, Portugal
"A Componente Estrutural do Sistema O" (TESE/DISSERTAÇÃO)
 Muito Bom
1991
Concluído
 Engenharia Electrotécnica e de Computadores (Licenciatura)
Universidade do Porto Faculdade de Engenharia, Portugal
 14
Percurso profissional

Ciência

Categoria Profissional
Instituição de acolhimento 		Empregador
2012/06/01 - Atual Investigador principal (carreira) (Investigação) Instituto de Engenharia de Sistemas e Computadores Tecnologia e Ciência Center for Research in Advanced Computing Systems, Portugal
Universidade do Minho, Portugal

Docência no Ensino Superior

Categoria Profissional
Instituição de acolhimento 		Empregador
2024/07/31 - Atual Professor Associado (Docente Universitário) Universidade do Minho, Portugal
Universidade do Minho Departamento de Informática, Portugal
1992/11/30 - Atual Professor Auxiliar (Docente Universitário) Universidade do Minho, Portugal
2003/06/20 - 2024/07/30 Professor Auxiliar (Docente Universitário) Universidade do Minho, Portugal
Universidade do Minho, Portugal
1994/03/01 - 2003/06/19 Assistente (Docente Universitário) Universidade do Minho, Portugal
1992/11/30 - 1994/02/28 Assistente Estagiário (Docente Universitário) Universidade do Minho, Portugal

Outros

Categoria Profissional
Instituição de acolhimento 		Empregador
1991/10/01 - 1992/09/30 Bolseiro de Mestrado JNICT - Programa Ciência Universidade do Minho, Portugal
Projetos

Projeto

Designação Financiadores
2018/07/04 - Atual REASSURE - Secure Runtime Verification for Reliable Real-Time Embedded Software
02/SAICT/2017 - NORTE-01-0145-FEDER-028550
Investigador
Associação para a Inovação e Desenvolvimento da FCT
Em curso
2021/02/01 - 2022/01/31 PassCert: Investigação do Impacto de Verificação Formal na Adopção de Software para Segurança de Passwords
CMU/TIC/0006/2019
Instituto de Engenharia de Sistemas e Computadores Investigação e Desenvolvimento em Lisboa, Portugal

Instituto de Engenharia de Sistemas e Computadores Tecnologia e Ciência, Portugal
Fundação para a Ciência e a Tecnologia
Em curso
2018/07/04 - 2021/07/03 Verificação em Tempo de Execução Segura para Software Embebido de Tempo-Real Confiável
PTDC/EEI-COM/28550/2017
Instituto Politécnico do Porto Instituto Superior de Engenharia do Porto, Portugal

Universidade do Minho, Portugal
Fundação para a Ciência e a Tecnologia
Em curso
2013/11/01 - 2016/10/31 PRACTICE - Privacy-Preserving Computation in the Cloud
Grant agreement ID: 609611
Investigador
European Commission Seventh Framework Programme for Research and Technological Development Information and Communication Technologies
Concluído
2010/06/01 - 2013/09/30 Secure Memories and Applications Related Technologies
info:eu-repo/grantAgreement/FCT/3599-PPCDT/116312/PT
Investigador
Fundação para a Ciência e a Tecnologia
Concluído
2010/06/01 - 2013/09/30 Memórias Seguras e Tecnologias Relacionadas com as suas Aplicações
ENIAC/2224/2009
Universidade do Minho Centro ALGORITMI, Portugal

Universidade do Minho, Portugal
Fundação para a Ciência e a Tecnologia
Concluído
2008/01/01 - 2011/03/31 RESCUE, REliable and Safe Code execUtion for Embedded systems
info:eu-repo/grantAgreement/FCT/5876-PPCDTI/65862/PT
Investigador
Fundação para a Ciência e a Tecnologia
Concluído
2008/01/01 - 2011/03/31 RESCUE, Execução Fiável e Segura de Programas em Sistemas Embebidos
PTDC/EIA/65862/2006
Universidade do Porto Laboratório de Inteligência Artificial e Ciência de Computadores, Portugal

Universidade do Porto Faculdade de Ciências, Portugal

Instituto Politécnico do Porto Instituto Superior de Engenharia do Porto, Portugal

Universidade do Minho, Portugal

Universidade da Beira Interior, Portugal
Fundação para a Ciência e a Tecnologia
Concluído
2008/01/01 - 2010/12/31 Computer Aided Cryptography Engineering
info:eu-repo/grantAgreement/EC/FP7/216499/EU
Investigador
Fundação para a Ciência e a Tecnologia
Concluído
2003/10/15 - 2007/01/14 PURe - Program Understanding and Re-engineering: Calculi and Applications
info:eu-repo/grantAgreement/FCT/Orçamento de Funcionamento/POSC/44304/PT
Investigador
Fundação para a Ciência e a Tecnologia
Concluído
Produções

Publicações

Artigo em conferência
  1. José Bacelar Almeida; Denis Firsov; Tiago Oliveira; Dominique Unruh. "Leakage-Free Probabilistic Jasmin Programs". 2025.
    10.1145/3703595.3705871
  2. José Bacelar Almeida; Santiago Arranz Olmos; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; et al. "Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt". 2024.
    10.1007/978-3-031-68379-4_12
  3. Grilo, M; Campos, J; Ferreira, JF; Almeida, JB; Mendes, A. "Verified Password Generation from Password Composition Policies". 2022.
    10.1007/978-3-031-07727-2_15
  4. Almeida, JB; Barbosa, M; Correia, ML; Eldefrawy, K; Lengrand, SG; Pacheco, H; Pereira, V. "Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head". 2021.
    10.1145/3460120.3484771
  5. Almeida, JB; Barbosa, M; Barthe, G; Grégoire, B; Koutsos, A; Laporte, V; Oliveira, T; Strub, PY. "The Last Mile: High-Assurance and High-Speed Cryptographic Implementations". 2020.
    10.1109/sp40000.2020.00028
  6. Almeida, JB; Barbosa, M; Barthe, G; Laporte, V; Oliveira, T. "Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification". 2020.
    10.1007/978-3-030-65277-7_6
  7. Almeida, JB; Baritel Ruet, C; Barbosa, M; Barthe, G; Dupressoir, F; Gregoire, B; Laporte, V; et al. "Machine-Checked Proofs for Cryptographic Standards Indifferentiability of SPONGE and Secure High-Assurance Implementations of SHA-3". 2019.
    10.1145/3319535.3363211
  8. Ramos, MVM; Bacelar Almeida, JCB; Moreira, N; de Queiroz, RJGB. "Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages". 2019.
    10.1016/j.entcs.2019.07.010
  9. Almeida, JB; Barbosa, M; Barthe, G; Campagna, M; Cohen, E; Gregoire, B; Pereira, V; et al. "A Machine-Checked Proof of Security for AWS Key Management Service". 2019.
    10.1145/3319535.3354228
  10. Almeida, JB; Cunha, A; Macedo, N; Pacheco, H; Proenca, J. "Teaching How to Program using Automated Assessment and Functional Glossy Games (Experience Report)". 2018.
    10.1145/3236777
  11. Almeida, JB; Barbosa, M; Barthe, G; Pacheco, H; Pereira, V; Portela, B. "Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks". Trabalho apresentado em 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, 2018.
    Publicado • 10.1109/CSF.2018.00017
  12. Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Gregoire, B; Laporte, V; Pereira, V. "A Fast and Verified Software Stack for Secure Function Evaluation". 2017.
    10.1145/3133956.3134017
  13. Almeida, JB; Barbosa, M; Barthe, G; Blot, A; Grégoire, B; Laporte, V; Oliveira, T; et al. "Jasmin: High-Assurance and High-Speed Cryptography". 2017.
    10.1145/3133956.3134078
  14. Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Emmi, M. "Verifying Constant-Time Implementations". 2016.
  15. Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F. "Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC". 2016.
    10.1007/978-3-662-52993-5_9
  16. Midena Ramos, MVM; de Queiroz, RJGB; Moreira, N; Bacelar Almeida, JCB. "On the Formalization of Some Results of Context-Free Language Theory". 2016.
    10.1007/978-3-662-52921-8_21
  17. Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F. "Certified computer-aided cryptography: Efficient provably secure machine code from high-level implementations". 2013.
    10.1145/2508859.2516652
  18. Barbosa, M; Almeida, JB; Pinto, JS; Vieira, B. "Deductive Verification of Cryptographic Software". 2009.
Artigo em revista
  1. Almeida, JB; Barbosa, M; Barthe, G; Grégoire, B; Laporte, V; Léchenet, JC; Oliveira, T; et al. "Formally verifying Kyber Episode IV: Implementation correctness". IACR Transactions on Cryptographic Hardware and Embedded System 3 (2023): 164-193.
    Acesso aberto • Publicado • 10.46586/tches.v2023.i3.164-193
  2. Bacelar Almeida, JC; Barbosa, M; Barthe, G; Pacheco, H; Pereira, V; Portela, B. "A formal treatment of the role of verified compilers in secure computation". Journal of Logical and Algebraic Methods in Programming (2022):
    10.1016/j.jlamp.2021.100736
  3. Ramos, MarcusViniciusMidena; Queiroz, RuyJ.G.B.de; Moreira, Nelma; Almeida, JoseCarlosBacelar. "Formalization of the Pumping Lemma for Context-Free Languages". JOURNAL OF FORMALIZED REASONING (2016):
    10.6092/issn.1972-5787/5595
  4. Almeida, J; Barbosa, M; Pacheco, H; Pereira, V. "A Tool-Chain for High-Assurance Cryptographic Software". ERCIM NEWS (2016): https://www.authenticus.pt/P-00K-XHG.
  5. Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F. "Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC". IACR Cryptology ePrint Archive (2015): https://www.authenticus.pt/P-00K-APA.
  6. Almeida, JB; Barbosa, M; Barthe, G; Davy, G; Dupressoir, F; Grégoire, B; Strub, PY. "Verified Implementations for Secure and Verifiable Computation". IACR Cryptology ePrint Archive (2014): https://www.authenticus.pt/P-00G-ANV.
  7. Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F. "Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations". IACR Cryptology ePrint Archive (2013): https://www.authenticus.pt/P-00G-ANW.
  8. Bacelar Almeida, J.; Barbosa, M.; Pinto, J.S.; Vieira, B.. "Formal verification of side-channel countermeasures using self-composition". Science of Computer Programming 78 7 (2013): 796-812. http://www.scopus.com/inward/record.url?eid=2-s2.0-84877581548&partnerID=MN8TOARS.
    10.1016/j.scico.2011.10.008
  9. Almeida, JB; Barbosa, M; Bangerter, E; Barthe, G; Krenn, S; Béguelin, SZ. "Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols". IACR Cryptology ePrint Archive (2012): https://www.authenticus.pt/P-00G-HTR.
  10. Almeida, J.B.; Barbosa, M.; Filliâtre, J.-C.; Pinto, J.S.; Vieira, B.. "CAOVerif: An open-source deductive verification platform for cryptographic software implementations". Science of Computer Programming (2012): http://www.scopus.com/inward/record.url?eid=2-s2.0-84867740990&partnerID=MN8TOARS.
    10.1016/j.scico.2012.09.019
  11. Almeida, J.B.; Barbosa, M.; Bangerter, E.; Barthe, G.; Krenn, S.; Béguelin, S.Z.. "Full proof cryptography: Verifiable compilation of efficient zero-knowledge protocols". Proceedings of the ACM Conference on Computer and Communications Security (2012): 488-500. http://www.scopus.com/inward/record.url?eid=2-s2.0-84869486464&partnerID=MN8TOARS.
    10.1145/2382196.2382249
  12. Almeida, J.B.; Moreira, N.; Pereira, D.; De Sousa, S.M.. "Partial derivative automata formalized in coq". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6482 LNCS (2011): 59-68. http://www.scopus.com/inward/record.url?eid=2-s2.0-79951613250&partnerID=MN8TOARS.
    10.1007/978-3-642-18098-9_7
  13. Almeida, JB; Bangerter, E; Barbosa, M; Krenn, S; Sadeghi, AR; Schneider, T. "A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols". IACR Cryptology ePrint Archive (2010): https://www.authenticus.pt/P-00G-ANZ.
  14. Almeida, J.B.; Bangerter, E.; Barbosa, M.; Krenn, S.; Sadeghi, A.-R.; Schneider, T.. "A certifying compiler for zero-knowledge proofs of knowledge based on ¿-protocols". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6345 LNCS (2010): 151-167. http://www.scopus.com/inward/record.url?eid=2-s2.0-78049411322&partnerID=MN8TOARS.
    10.1007/978-3-642-15497-3_10
  15. Almeida, J.B.; Barbosa, M.; Pinto, J.S.; Vieira, B.. "Deductive verification of cryptographic software". Innovations in Systems and Software Engineering 6 3 (2010): 203-218. http://www.scopus.com/inward/record.url?eid=2-s2.0-77956423308&partnerID=MN8TOARS.
    10.1007/s11334-010-0127-y
  16. Almeida, J.B.; Barbosa, M.; Sousa Pinto, J.; Vieira, B.. "Verifying cryptographic software correctness with respect to reference implementations". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 5825 LNCS (2009): 37-52. http://www.scopus.com/inward/record.url?eid=2-s2.0-70549106955&partnerID=MN8TOARS.
    10.1007/978-3-642-04570-7_5
  17. Almeida, J.B.; Pinto, J.S.; Vilaça, M.. "Token-passing Nets for Functional Languages". Electronic Notes in Theoretical Computer Science 204 C (2008): 181-198. http://www.scopus.com/inward/record.url?eid=2-s2.0-41649083728&partnerID=MN8TOARS.
    10.1016/j.entcs.2008.03.061
  18. Almeida, J.B.; Pinto, J.S.; Vilaça, M.. "A Tool for Programming with Interaction Nets". Electronic Notes in Theoretical Computer Science 219 C (2008): 83-96. http://www.scopus.com/inward/record.url?eid=2-s2.0-55749108664&partnerID=MN8TOARS.
    10.1016/j.entcs.2008.10.036
  19. Almeida, J.B.; Pinto, J.S.; Vilaça, M.. "A Local Graph-rewriting System for Deciding Equality in Sum-product Theories". Electronic Notes in Theoretical Computer Science 176 1 (2007): 139-163. http://www.scopus.com/inward/record.url?eid=2-s2.0-34248563510&partnerID=MN8TOARS.
    10.1016/j.entcs.2006.10.031
  20. Almeida, J.B.; Almeida, P.S.; Baquero, C.. "Bounded version vectors". Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 3274 (2004): 102-116. http://www.scopus.com/inward/record.url?eid=2-s2.0-35048864528&partnerID=MN8TOARS.
    10.1007/978-3-540-30186-8_8
Livro
  1. Almeida, José Bacelar; Frade, Maria João; Pinto, Jorge Sousa; Melo de Sousa, Simão. Rigorous Software Development. Londres, Reino Unido: Springer-Verlag. 2011.
    10.1007/978-0-85729-018-2

Outros

Outra produção
  1. A Machine-Checked Proof of Security for AWS Key Management Service. 2019. Almeida, JB; Barbosa, M; Barthe, G; Campagna, M; Cohen, E; Grégoire, B; Pereira, V; et al.
  2. Formalization of context-free language theory. 2015. Ramos, MarcusV.M.; Queiroz, RuyJ.G.B.de; Moreira, Nelma; Almeida, JoseCarlosBacelar.
  3. Deriving Sorting Algorithms. 2008. Almeida, JoseBacelar; Pinto, JorgeSousa. https://www.authenticus.pt/P-00G-6CG.
Atividades

Orientação

Título / Tema
Papel desempenhado 		Curso (Tipo)
Instituição / Organização
2022/01/31 - Atual High-Assurance Post-Quantum Cryptography and Distributed Secure Computation
Orientador
 Programa Doutoral em Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2017/09/01 - 2023 Extending Conflict-Free Repiclated Data Types fault models
Coorientador
 Informática (Doutoramento)
Universidade do Minho, Portugal
2015/10/01 - 2022/09/05 High-speed, high-assurance Cryptography
Coorientador
 Programa Doutoral MAP/i (Doutoramento)
Universidade do Porto Faculdade de Ciências, Portugal
2020/10/01 - 2022/07/27 PAdES Server Signer
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho, Portugal
2020/10/01 - 2022/07/06 Traceability and Safety Tradeoffs in Modern Vehicles
Orientador
 Mestrado Integrado em Engenharia Informática (Mestrado)
Universidade do Minho, Portugal
2020/10/01 - 2022/04/21 Icarus - A Cloud Security Perspective
Orientador
 Mestrado em Engenharia Informática (Mestrado)
2020/10/01 - 2022/04/21 Implementação Certificada da Componente Criptográfica do Gestor de Passwords KeePass
Orientador
 Mestrado Integrado em Engenharia Informática (Mestrado)
Universidade do Minho, Portugal
2020/10/01 - 2022/04/05 Quantum Error-Correcting Codes
Coorientador
 Mestrado em Engenharia Física (Mestrado)
2020/10/01 - 2021/11/15 Formal Verification of Password Generation Algorithms used in Password Managers
Coorientador
 Mestrado em Sistemas de Informação e Engenharia de Computadores (Mestrado)
Universidade de Lisboa Instituto Superior Técnico, Portugal
2020/10/01 - 2021/11/05 Self-Sovereign Identity - Decentralized Identifiers, Claims and Credentials using non Decentralized Ledger Technology
Orientador
 Mestrado Integrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2020/10/01 - 2021/10/25 Gestão de Segurança de Informação para Sistemas de Confiança Seguros
Orientador
 Mestrado Integrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2019/10/01 - 2021/05/12 DIDs, Claims, Credentials e Blockchains (Self-sovereign Identity)
Orientador
 Mestrado Integrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2019/10/01 - 2021/04/21 eIDAS Qualified Trust Services Serviço de Preservação
Orientador
 Mestrado Integrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2019/10/01 - 2021/03/22 Privacy and Security in Data Mining
Orientador
 Mestrado Integrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2019/10/01 - 2020/12/17 Formal Verification in Blockchains and Related Technologies - Using Agda to prove liveness of Consensus Algorithms
Orientador
 Mestrado Integrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Arquitetura, Portugal
2019/10/01 - 2020/09/24 Esquemas de assinatura digital Lattice-based e experimentação de certificados híbridos com criptografia pós-quântica
Coorientador
 Mestrado em Matemática e Computação (Mestrado)
Universidade do Minho Escola de Ciências, Portugal
2019/10/01 - 2020/07/14 TrustZone based Attestation in Secure Runtime Verification for Embedded Systems
Orientador
 Mestrado Integrado em Engenharia Informática (Mestrado)
2018/10/01 - 2020/05/15 Cloud Computing and GDPR - legal and technical implications of the new regulation on SAAS in the Portuguese context
Coorientador
 Mestrado em Direito e Informática (Mestrado)
Universidade do Minho Escola de Direito, Portugal
2015/10/01 - 2020/04/29 Integrated Verification of Cryptographic Security Proofs and Implementations
Coorientador de Vitor Manuel Parreira Pereira
 Programa Doutoral MAP/i (Doutoramento)
Universidade do Porto Faculdade de Ciências, Portugal
2018/10/01 - 2019/12/09 Conveniência e Segurança com SCMD
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2018/10/01 - 2019/12/09 Desmaterialização de documentos de identificação
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2018/10/01 - 2019/07/22 Uma abordagem criptográfica a sistemas eleitorais
Coorientador
 Mestrado em Matemática e Computação (Mestrado)
Universidade do Minho Escola de Ciências, Portugal
2017/10/01 - 2018/11/20 eHealth: Segurança, Privacidade e Protecção de Dados Pessoais no Setor da Saúde
Coorientador
 Mestrado em Direito e Informática (Mestrado)
Universidade do Minho Escola de Direito, Portugal
2017/10/01 - 2018/10/09 Sistemas de deteção de Branqueamento de Capitais
Coorientador
 Mestrado em Direito e Informática (Mestrado)
Universidade do Minho Escola de Direito, Portugal
2016/10/01 - 2017/12/19 Transações Seguras com BlockChains
Coorientador
 Mestrado em Matemática e Computação (Mestrado)
Universidade do Minho Escola de Ciências, Portugal
2015/11/01 - 2017/06/28 Computação distribuída segura na presença de adversários ativos
Orientador
 Engenharia Informática (Mestrado)
Universidade do Minho, Portugal
2015/10/01 - 2017/06/28 Computação Segura Sobre Sistemas de Dados em Ambientes Cloud
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2015/11/01 - 2017/01/23 geração de descrições de computação para a cloud
Orientador
 Engenharia Informática (Mestrado)
Universidade do Minho, Portugal
2015/11/01 - 2016/12/14 Análise de segurança para soluções de software para a cloud
Orientador
 Engenharia Informática (Mestrado)
Universidade do Minho, Portugal
2015/10/01 - 2016/12/14 Análise de Segurança para Soluções de Software para a Cloud
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2014/10/01 - 2015/12/16 Public Keys Quality
Coorientador
 Mestrado em Matemática e Computação
Universidade do Minho Escola de Ciências, Portugal
2014/10/01 - 2015/09/25 A deductive verification tool for cryptographic software
Coorientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2013/10/01 - 2015/03/13 Secure Multiparty Computation Protocols
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2013/11/01 - 2014/12/19 A Máquina Abstracta Categorial
Coorientador
 Matemática e Computação (Mestrado)
Universidade do Minho, Portugal
2012/10/01 - 2014/04/04 Cryptographic Library Support for a Certified Compiler
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2012/10/01 - 2014/03/20 Dos Testemunhos de Conexão no Quadro Legislativo Europeu da Proteção de Dados - em particular do consentimento para a sua utilização
Coorientador
 Mestrado em Direito e Informática (Mestrado)
Universidade do Minho Escola de Direito, Portugal
2012/11/01 - 2013/09/27 Reforço da privacidade através do controlo da pegada digital
Orientador
 Engenharia Informática (Mestrado)
Universidade do Minho, Portugal
2011/11/01 - 2013/04/03 O impacto da computação quântica na criptografia moderna
Orientador
 Engenharia Informática (Mestrado)
Universidade do Minho, Portugal
2011/11/01 - 2013/04/03 Remote electronic voting : studying and improving Helios
Orientador
 Engenharia Informática (Mestrado)
Universidade do Minho, Portugal
2011/10/01 - 2012/12/21 Implementação de funções de hash e cifras de chave pública baseadas em retículos
Coorientador
 Mestrado em Matemática e Computação (Mestrado)
Universidade do Minho Escola de Ciências, Portugal
2010/10/01 - 2012/04/05 Domain-specific Languages for Cryptographic Software
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2010/10/01 - 2012/04/05 Finite Probability Distributions in Coq
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2010/10/01 - 2011/12/14 Ferramentas de Verificação Formal de Protocolos Criptográficos
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2009/10/01 - 2010/12/16 Extensões de Alto Nível para uma Linguagem de Programação Criptográfica
Orientador
 Mestrado em Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2009/10/01 - 2010/09/30 Formal Verification of Security Proofs
Orientador
 Mestrado em Engenharia Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2007/10/01 - 2009/01/16 Preservação de Privacidade Apelando a Técnicas de Mineração de Dados
Orientador
 Mestrado em Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
2007/10/01 - 2009/01/10 On the implementation of cryptographic algorithms in Java
Orientador
 Mestrado em Informática (Mestrado)
Universidade do Minho Escola de Engenharia, Portugal
Distinções

Prémio

2016 Best Paper Award at Fast Software Encryption 2016
2009 Best Software Science paper presented at the FMICS'09