???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; .
Read full resume ↓
Identification

Personal identification

Full name
José Carlos Bacelar Almeida

Citation names

  • Almeida, José Bacelar

Author identifiers

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

Knowledge fields

  • Exact Sciences - Computer and Information Sciences - Computer Sciences

Languages

Language Speaking Reading Writing Listening Peer-review
English Intermediate (B1) Advanced (C1) Intermediate (B1) Intermediate (B1)
French Beginner (A1) Intermediate (B1) Beginner (A1) Beginner (A1)
Spanish; Castilian Beginner (A1) Beginner (A1) Beginner (A1) Beginner (A1)
Education
Degree Classification
2003
Concluded
 Doutoramento em Informática (Doutoramento)
Universidade do Minho Escola de Engenharia, Portugal
"Uma Abordagem à Verificação Automática de Protocolos Criptográficos" (THESIS/DISSERTATION)
 Aprovado
1994
Concluded
 Mestrado em Informática (Mestrado)
Universidade do Minho, Portugal
"A Componente Estrutural do Sistema O" (THESIS/DISSERTATION)
 Muito Bom
1991
Concluded
 Engenharia Electrotécnica e de Computadores (Licenciatura)
Universidade do Porto Faculdade de Engenharia, Portugal
 14
Affiliation

Science

Category
Host institution 		Employer
2012/06/01 - Current Principal Investigator (Research) Instituto de Engenharia de Sistemas e Computadores Tecnologia e Ciência Center for Research in Advanced Computing Systems, Portugal
Universidade do Minho, Portugal

Teaching in Higher Education

Category
Host institution 		Employer
2024/07/31 - Current Associate Professor (University Teacher) Universidade do Minho, Portugal
Universidade do Minho Departamento de Informática, Portugal
1992/11/30 - Current Assistant Professor (University Teacher) Universidade do Minho, Portugal
2003/06/20 - 2024/07/30 Assistant Professor (University Teacher) Universidade do Minho, Portugal
Universidade do Minho, Portugal
1994/03/01 - 2003/06/19 Assistant (University Teacher) Universidade do Minho, Portugal
1992/11/30 - 1994/02/28 Trainee Assistant (University Teacher) Universidade do Minho, Portugal

Others

Category
Host institution 		Employer
1991/10/01 - 1992/09/30 Bolseiro de Mestrado JNICT - Programa Ciência Universidade do Minho, Portugal
Projects

Contract

Designation Funders
2018/07/04 - Current REASSURE - Secure Runtime Verification for Reliable Real-Time Embedded Software
02/SAICT/2017 - NORTE-01-0145-FEDER-028550
Researcher
Associação para a Inovação e Desenvolvimento da FCT
Ongoing
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
Ongoing
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
Ongoing
2013/11/01 - 2016/10/31 PRACTICE - Privacy-Preserving Computation in the Cloud
Grant agreement ID: 609611
Researcher
European Commission Seventh Framework Programme for Research and Technological Development Information and Communication Technologies
Concluded
2010/06/01 - 2013/09/30 Secure Memories and Applications Related Technologies
info:eu-repo/grantAgreement/FCT/3599-PPCDT/116312/PT
Researcher
Fundação para a Ciência e a Tecnologia
Concluded
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
Concluded
2008/01/01 - 2011/03/31 RESCUE, REliable and Safe Code execUtion for Embedded systems
info:eu-repo/grantAgreement/FCT/5876-PPCDTI/65862/PT
Researcher
Fundação para a Ciência e a Tecnologia
Concluded
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
Concluded
2008/01/01 - 2010/12/31 Computer Aided Cryptography Engineering
info:eu-repo/grantAgreement/EC/FP7/216499/EU
Researcher
Fundação para a Ciência e a Tecnologia
Concluded
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
Researcher
Fundação para a Ciência e a Tecnologia
Concluded
Outputs

Publications

Book
  1. Almeida, José Bacelar; Frade, Maria João; Pinto, Jorge Sousa; Melo de Sousa, Simão. Rigorous Software Development. Londres, United Kingdom: Springer-Verlag. 2011.
    10.1007/978-0-85729-018-2
Conference paper
  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". Paper presented in 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, 2018.
    Published • 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.
Journal article
  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.
    Open access • Published • 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

Other

Other output
  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.
Activities

Supervision

Thesis Title
Role 		Degree Subject (Type)
Institution / Organization
2022/01/31 - Current High-Assurance Post-Quantum Cryptography and Distributed Secure Computation
Supervisor
 Programa Doutoral em Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2017/09/01 - 2023 Extending Conflict-Free Repiclated Data Types fault models
Co-supervisor
 Informática (PhD)
Universidade do Minho, Portugal
2015/10/01 - 2022/09/05 High-speed, high-assurance Cryptography
Co-supervisor
 Programa Doutoral MAP/i (PhD)
Universidade do Porto Faculdade de Ciências, Portugal
2020/10/01 - 2022/07/27 PAdES Server Signer
Supervisor
 Mestrado em Engenharia Informática (Master)
Universidade do Minho, Portugal
2020/10/01 - 2022/07/06 Traceability and Safety Tradeoffs in Modern Vehicles
Supervisor
 Mestrado Integrado em Engenharia Informática (Master)
Universidade do Minho, Portugal
2020/10/01 - 2022/04/21 Icarus - A Cloud Security Perspective
Supervisor
 Mestrado em Engenharia Informática (Master)
2020/10/01 - 2022/04/21 Implementação Certificada da Componente Criptográfica do Gestor de Passwords KeePass
Supervisor
 Mestrado Integrado em Engenharia Informática (Master)
Universidade do Minho, Portugal
2020/10/01 - 2022/04/05 Quantum Error-Correcting Codes
Co-supervisor
 Mestrado em Engenharia Física (Master)
2020/10/01 - 2021/11/15 Formal Verification of Password Generation Algorithms used in Password Managers
Co-supervisor
 Mestrado em Sistemas de Informação e Engenharia de Computadores (Master)
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
Supervisor
 Mestrado Integrado em Engenharia Informática (Master)
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
Supervisor
 Mestrado Integrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2019/10/01 - 2021/05/12 DIDs, Claims, Credentials e Blockchains (Self-sovereign Identity)
Supervisor
 Mestrado Integrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2019/10/01 - 2021/04/21 eIDAS Qualified Trust Services Serviço de Preservação
Supervisor
 Mestrado Integrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2019/10/01 - 2021/03/22 Privacy and Security in Data Mining
Supervisor
 Mestrado Integrado em Engenharia Informática (Master)
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
Supervisor
 Mestrado Integrado em Engenharia Informática (Master)
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
Co-supervisor
 Mestrado em Matemática e Computação (Master)
Universidade do Minho Escola de Ciências, Portugal
2019/10/01 - 2020/07/14 TrustZone based Attestation in Secure Runtime Verification for Embedded Systems
Supervisor
 Mestrado Integrado em Engenharia Informática (Master)
2018/10/01 - 2020/05/15 Cloud Computing and GDPR - legal and technical implications of the new regulation on SAAS in the Portuguese context
Co-supervisor
 Mestrado em Direito e Informática (Master)
Universidade do Minho Escola de Direito, Portugal
2015/10/01 - 2020/04/29 Integrated Verification of Cryptographic Security Proofs and Implementations
Co-supervisor of Vitor Manuel Parreira Pereira
 Programa Doutoral MAP/i (PhD)
Universidade do Porto Faculdade de Ciências, Portugal
2018/10/01 - 2019/12/09 Conveniência e Segurança com SCMD
Supervisor
 Mestrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2018/10/01 - 2019/12/09 Desmaterialização de documentos de identificação
Supervisor
 Mestrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2018/10/01 - 2019/07/22 Uma abordagem criptográfica a sistemas eleitorais
Co-supervisor
 Mestrado em Matemática e Computação (Master)
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
Co-supervisor
 Mestrado em Direito e Informática (Master)
Universidade do Minho Escola de Direito, Portugal
2017/10/01 - 2018/10/09 Sistemas de deteção de Branqueamento de Capitais
Co-supervisor
 Mestrado em Direito e Informática (Master)
Universidade do Minho Escola de Direito, Portugal
2016/10/01 - 2017/12/19 Transações Seguras com BlockChains
Co-supervisor
 Mestrado em Matemática e Computação (Master)
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
Supervisor
 Engenharia Informática (Master)
Universidade do Minho, Portugal
2015/10/01 - 2017/06/28 Computação Segura Sobre Sistemas de Dados em Ambientes Cloud
Supervisor
 Mestrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2015/11/01 - 2017/01/23 geração de descrições de computação para a cloud
Supervisor
 Engenharia Informática (Master)
Universidade do Minho, Portugal
2015/11/01 - 2016/12/14 Análise de segurança para soluções de software para a cloud
Supervisor
 Engenharia Informática (Master)
Universidade do Minho, Portugal
2015/10/01 - 2016/12/14 Análise de Segurança para Soluções de Software para a Cloud
Supervisor
 Mestrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2014/10/01 - 2015/12/16 Public Keys Quality
Co-supervisor
 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
Co-supervisor
 Mestrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2013/10/01 - 2015/03/13 Secure Multiparty Computation Protocols
Supervisor
 Mestrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2013/11/01 - 2014/12/19 A Máquina Abstracta Categorial
Co-supervisor
 Matemática e Computação (Master)
Universidade do Minho, Portugal
2012/10/01 - 2014/04/04 Cryptographic Library Support for a Certified Compiler
Supervisor
 Mestrado em Engenharia Informática (Master)
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
Co-supervisor
 Mestrado em Direito e Informática (Master)
Universidade do Minho Escola de Direito, Portugal
2012/11/01 - 2013/09/27 Reforço da privacidade através do controlo da pegada digital
Supervisor
 Engenharia Informática (Master)
Universidade do Minho, Portugal
2011/11/01 - 2013/04/03 O impacto da computação quântica na criptografia moderna
Supervisor
 Engenharia Informática (Master)
Universidade do Minho, Portugal
2011/11/01 - 2013/04/03 Remote electronic voting : studying and improving Helios
Supervisor
 Engenharia Informática (Master)
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
Co-supervisor
 Mestrado em Matemática e Computação (Master)
Universidade do Minho Escola de Ciências, Portugal
2010/10/01 - 2012/04/05 Domain-specific Languages for Cryptographic Software
Supervisor
 Mestrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2010/10/01 - 2012/04/05 Finite Probability Distributions in Coq
Supervisor
 Mestrado em Engenharia Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2010/10/01 - 2011/12/14 Ferramentas de Verificação Formal de Protocolos Criptográficos
Supervisor
 Mestrado em Engenharia Informática (Master)
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
Supervisor
 Mestrado em Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2009/10/01 - 2010/09/30 Formal Verification of Security Proofs
Supervisor
 Mestrado em Engenharia Informática (Master)
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
Supervisor
 Mestrado em Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
2007/10/01 - 2009/01/10 On the implementation of cryptographic algorithms in Java
Supervisor
 Mestrado em Informática (Master)
Universidade do Minho Escola de Engenharia, Portugal
Distinctions

Award

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