supervisions

Doctoral, masters and undergraduate students supervised, their theses, and Ph.D. examinations as external examiner.

Ph.D. (current)

  1. Farias, B. Bounded Dynamic Semantics for Python Programs. In: Ph.D. in Computer Science, University of Manchester, 2024-2027 (Supervisor).
  2. Abacha, F. Secure Sharing of Dynamic Data via Privacy-Preserving Distributed Learning Framework. In: Ph.D. in Computer Science, University of Manchester, 2023-2026 (Co-Supervisor).
  3. Zhu, T. Software Testing with Large Language Models. In: Ph.D. in Computer Science, University of Manchester, 2023-2026 (Co-Supervisor).

Ph.D. (graduated)

  1. Wu, T. Efficient Concurrent Software Verification with Bounded Model Checking and Deep Learning. In: Ph.D. in Computer Science, University of Manchester, 2026 (Supervisor).
  2. Menezes, R. S. A Formal Semantics for GOTO in the CProver Ecosystem. In: Ph.D. in Computer Science, University of Manchester, 2025 (Supervisor).
  3. Aldughaim, M. A. Interval Analysis and Methods in Software Analysis. In: Ph.D. in Computer Science, University of Manchester, 2025 (Supervisor).
  4. Matos Jr, J. B. P. An Automated Method for Neural Network Quantization Refinement. In: Ph.D. in Informatics, Federal University of Amazonas, 2025 (Supervisor).
  5. Song, X. Automated Verification and Repair of Quantized Neural Networks. In: Ph.D. in Computer Science, University of Manchester, 2024 (Co-Supervisor).
  6. Erdayandi, K. Privacy-Preserving Trading in Local Energy Markets. In: Ph.D. in Computer Science, University of Manchester, 2024 (Co-Supervisor).
  7. Aljaafari, F. K. Black-Box Cooperative Verification Framework For Finding Software Vulnerabilities in Concurrent Programs. In: Ph.D. in Computer Science, University of Manchester, 2023 (Supervisor).
  8. Alshmrany, K. M. Efficient Hybrid Fuzzing for Detecting Vulnerabilities and Achieving High Coverage in Software. In: Ph.D. in Computer Science, University of Manchester, 2023 (Supervisor).
  9. Sakr, M. Fine-Grained Forgetting for Expressive Description Logics: Deductive, Semantic, and Query Forgetting in One Framework. In: Ph.D. in Computer Science, University of Manchester, 2023 (Co-Supervisor).
  10. Romero, M. J. Understanding the Microeconomic Impact of Automation in Digital Organisations. In: Ph.D. in Computer Science, University of Manchester, 2023 (Co-Supervisor).
  11. Trajanovski, T. Countering IoT Botnets. In: Ph.D. in Computer Science, University of Manchester, 2023 (Co-Supervisor).
  12. Thayaparan, M. Differentiable Constraint-based Solvers for Explanation-based Multi-hop Inference. In: Ph.D. in Computer Science, University of Manchester, 2023 (Co-Supervisor).
  13. Trindade, A. B. Automated Verification of Stand-alone Solar Photovoltaic Systems. In: D.Sc. in Informatics, Federal University of Amazonas, 2020 (Supervisor).
  14. Rocha, H. O. Verificação de Sistemas de Software baseada em Transformações de Código usando Bounded Model Checking. In: D.Sc. in Informatics, Federal University of Amazonas, 2015 (Co-Supervisor).

M.Phil.

  1. Zhang, W. Modelling Explanatory Reasoning: A Study on Explanatory Patterns and Graph-Based Inference. In: M.Phil. in Computer Science, University of Manchester, 2025 (Co-Supervisor).
  2. Blanaru, F.-G. Data Transfer Optimizations for Heterogeneous Managed Runtime Systems. In: M.Phil. in Computer Science, University of Manchester, 2022 (Co-Supervisor).
  3. Alhawi, O. Finding Software Vulnerabilities in Unmanned Aerial Vehicles Using Software Verification. In: M.Phil. in Computer Science, University of Manchester, 2021 (Supervisor).

M.Sc.

  1. Santos, E. J. C. Detecção de Ataques de Negação de Serviço em Inversores Fotovoltaicos Conectados à Internet: Uma Abordagem por Ensemble de Aprendizagem de Máquina. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2026 (Co-Supervisor).
  2. Deveza, J. S. Técnicas de contracão de domínio de variáveis em verificação formal e detecção de vulnerabilidades de software usando programação por restrições e aritmética intervalar. In: M.Sc. in Informatics, Federal University of Amazonas, 2024 (Co-Supervisor).
  3. de Sousa, J. O. LSVerifier: A BMC Approach to Identify Security Vulnerabilities in C Open-Source Software. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2023 (Supervisor).
  4. Hong. H. Verifying Quantized Neural Networks using SMT-Based Model Checking. In: M.Sc. in Advanced Computer Science, University of Manchester, 2023 (Supervisor).
  5. Li, x. Safety Verification of CUDA and Deep Neural Networks. In: M.Sc. in Advanced Computer Science, University of Manchester, 2023 (Supervisor).
  6. Cheng, Z. Develop and Evaluate a Security Analyzer for Finding Vulnerabilities in Java programs. In: M.Sc. in Advanced Computer Science, University of Manchester, 2023 (Supervisor).
  7. Zhou, Z. The ESBMC-based Approach to Security Verification in Linux Kernel Programs. In: M.Sc. in Advanced Computer Science, University of Manchester, 2023 (Supervisor).
  8. Salim, B. ESBMC-based Ethereum Smart Contract Security Verification. In: M.Sc. in Advanced Computer Science, University of Manchester, 2022 (Supervisor).
  9. Wu, C. Fuzzing a Software Verifier. In: M.Sc. in Advanced Computer Science, University of Manchester, 2022 (Supervisor).
  10. Li, M. Incremental Bounded Model Checking using Machine Learning Techniques. In: M.Sc. in Advanced Computer Science, University of Manchester, 2022 (Supervisor).
  11. Young, J. Verifying Binarised Neural Networks using SMT-Based Model Checking. In: M.Sc. in Advanced Computer Science, University of Manchester, 2022 (Supervisor).
  12. Lu, Y. Scaling up Bounded-Model-Checking for Internet of Things devices. In: M.Sc. in Advanced Computer Science, University of Manchester, 2022 (Supervisor).
  13. Sena, L. H. C. Automated Verification and Refutation of Quantized Neural Networks. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2022 (Supervisor).
  14. He, H. Incremental Bounded Model Checking using Machine Learning Techniques. In: M.Sc. in Advanced Computer Science, University of Manchester, 2021 (Supervisor).
  15. Wang, S. Develop and Evaluate a Security Analyzer for Finding Vulnerabilities in Java programs. In: M.Sc. in Advanced Computer Science, University of Manchester, 2021 (Supervisor).
  16. Wu, T. Develop and Evaluate a Security Analyzer for Finding Vulnerabilities in Java programs. In: M.Sc. in Advanced Computer Science, University of Manchester, 2021 (Supervisor).
  17. Song, K. SMT-Based Bounded Model Checking for Solidity Smart Contracts. In: M.Sc. in Advanced Computer Science, University of Manchester, 2021 (Supervisor).
  18. Matulevicius, N. Verifying Information Flow Security for Blockchain-based Smart Contracts. In: M.Sc. in Advanced Computer Science, University of Manchester, 2021 (Supervisor).
  19. Menezes, R. S. Geração de Casos de Teste Usando Bounded Model Checking. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2020 (supervisor).
  20. Tan, V. L. Security Analyser Tool for Finding Vulnerabilities in Java Programs. In: M.Sc. in Advanced Computer Science, University of Manchester, 2020 (Supervisor).
  21. Monteiro, F. R. Formal Verification to Ensuring the Memory Safety of C++ Programs. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2020 (supervisor).
  22. de Souza, A. S. Verificação de Programas Multi-Tarefas Baseado no Framework Multiplataforma QT. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2019 (supervisor).
  23. Alkhamissi, S. R. **Finding Software Vulnerabilities in Unmanned Aerial Vehicles. In: M.Sc. in Advanced Computer Science, University of Manchester, 2019 (Supervisor).
  24. Cavalcante, T. R. F. Verificação e Síntese de Controladores de Realimentação de Estados Estática com Garantias Formais de Desempenho Não Frágil. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2019 (co-supervisor).
  25. Albuquerque, H. F. Uma abordagem de otimização guiada por contra-exemplos usando solucionadores SAT e SMT. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2019 (supervisor).
  26. Pereira, P. A. Verificação Limitada de Modelos Baseada em SMT para Programas CUDA. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2019 (supervisor).
  27. Alves, E. H. S. Localização de Falhas em Programas Concorrentes em C. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2018 (co-supervisor).
  28. Chaves, L. C. Formal Verification Applied to Attitude Control Software of Unmanned Aerial Vehicles. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2018 (supervisor).
  29. de Melo, R. W. R. Verificação de Programas Embarcados ANSI-C Baseada em Indução Matemática e Invariantes.. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2017 (supervisor).
  30. Garcia, M. A. P. Verificação de Programas C++ Baseados no Framework Cross-Platform Qt. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2016 (supervisor).
  31. Ismail, H. I. Verificação de Modelos Aplicada ao Projeto de Controladores Digitais Implementados em Processadores de Ponto-Fixo. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2015 (supervisor).
  32. Januário, F. A. P. BMCLua: Metodologia para Verificação de Códigos Lua Utilizando Bounded Model Checking. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2015 (supervisor).
  33. Trindade, A. B. Aplicando Verificação Formal Baseada nas Teorias do Módulo da Satisfabilidade para o Particionamento de Hardware/Software em Sistemas Embarcados. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2015 (supervisor). [Resumo]
  34. Abreu, R. B. Avaliação de Projetos de Filtros Digitais de Ponto-Fixo usando Teorias do Módulo da Satisfatibilidade. In: M.Sc. in Electrical Engineering , Federal University of Amazonas, 2014 (supervisor).
  35. Gadelha, M. Y. R. Verificação Baseada em Indução Matemática para Programas C++. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2013 (supervisor).

B.Sc.

  1. Moura, D. **Investigando as Relações Entre Problemas de Segurança de Memória e Desempenho em Programas Kotlin. In: B.Sc. in Electrical Engineering, Federal University of Amazonas, 2023 (supervisor).
  2. Gotkowicz, M. **Grammar-Aware MQTT Fuzzing. In: B.Sc. in Computer Science, University of Manchester, 2022 (supervisor).
  3. Lu, W. **Verifying Python Programs in Robotic Applications. In: B.Sc. in Computer Science, University of Manchester, 2022 (supervisor).
  4. Li, M. **Counterexample-Guided Optimisation Applied to Mobile Robot Path Planning. In: B.Sc. in Computer Science, University of Manchester, 2021 (supervisor).
  5. Kung, Y. S. Counterexample Guided Inductive Optimisation. In: B.Sc. in Computer Science, University of Manchester, 2020 (supervisor).
  6. Balan, A. C. A Security Analyser for Finding Vulnerabilities in C Programs. In: B.Sc. in Computer Science, University of Manchester, 2020 (supervisor).
  7. Mihai, L. Counterexample-Guided Optimisation Applied to Mobile Robot Path Planning. In: B.Sc. in Computer Science, University of Manchester, 2020 (supervisor).
  8. Chitoraga, D. Assisted Counterexample Guided Optimisation. In: B.Sc. in Artificial Intelligence, University of Manchester, 2019 (supervisor).
  9. Albuquerque, H. F. Modelo Operacional CUDA para Verificação de Programas. In: B.Eng. in Computer Engineering, Federal University of Amazonas, 2016 (supervisor).
  10. Sousa, F. R., Verificação de Controladores Digitais de Ponto Fixo Representados por Espaço de Estados. In: Institutional Scientific Initiation Program, Federal University of Amazonas, 2015 (supervisor).
  11. Pereira, P. A. Desenvolvimento de um Modelo em VHDL para Avaliação de Corretude e Desempenho do Processador MIPS usando Arquiteturas Baseadas em Multiciclo e Pipeline. In: B.Eng. in Computer Engineering, Federal University of Amazonas, 2015 (supervisor).
  12. Alves, E. H. S. Um Método para Localizar Falhas em Software Concorrente em C. In: B.Eng. in Computer Engineering, Federal University of Amazonas, 2015 (supervisor).
  13. Sousa, F. R. Verificação de Programas C++ que Usam o Framework Multiplataforma QT. In: Institutional Scientific Initiation Program, Federal University of Amazonas, 2013 (supervisor).

Ph.D. examinations

I acted as an external examiner for the following Ph.D. candidates:

  1. Bamohabbat Chafjiri, S. Advancing Software Fuzzing Techniques Through the Exploration of Cryptographic Concepts and Machine Learning, 2025. University of the West of England, UK.
  2. Matos Jr, J. B. P. An Automated Method for Neural Network Quantization Refinement, 2025. Federal University of Amazonas, Brazil.
  3. Alon, Y. Neural Reasoning for Program Analysis, 2025. University of Bristol, UK.
  4. Almutairi, H. A Swarm Intelligence-Based Path Selection for Low-Power and Lossy Networks with the Presence of Packet Dropping Attacks, 2024. University of Manchester, UK.
  5. Chen, Y. On More Effective Performance Testing, 2023. Lancaster University, UK.
  6. Chatterjee, P. Efficient Verification And Testing Of Software Systems Using Proofs Of Unsatisfiability And Multiverse Analysis, 2023. Indian Institute of Technology Kanpur, India.
  7. Rodriguez, L. G. A. Mechanisms to Improve Fuzz Testing for Message Brokers, 2023. University of São Paulo, Brazil.
  8. Tay, S. W. A Two-Level Communication-Based Access Control Framework for the Internet Of Things, 2022. University of Manchester, UK.
  9. Peng, C. Automated Testing for GPU Kernels, 2021. University of Edinburgh, UK.
  10. Di Stefano, L. Modelling and Verification of Multi-Agent Systems via Sequential Emulation, 2020. Gran Sasso Science Institute, Italy.
  11. Klimis, V. Abstractions and Optimisations for Model-Checking Software-Defined Networks, 2020. University of Essex, UK.
  12. Valentin, E. B. Scheduling Hard Real-Time Tasks in Heterogeneous Multiprocessor Platforms subject to Energy and Temperature Constraints, 2017. Federal University of Amazonas, Brazil.
  13. Dias, J. R. S. Métodos de Controle de Fluxo de Entrada para Sistemas Modelados por Grafos de Eventos Temporizados, 2014. Federal University of Minas Gerais, Brazil.