supervisions

Doctoral, masters and undergraduate students supervised, and their theses.

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).
  4. Wu, T. Hybrid Fuzzing Concurrent Software using Model Checking and Machine Learning. In: Ph.D. in Computer Science, University of Manchester, 2022-2026 (Supervisor).

Ph.D. (graduated)

  1. Menezes, R. S. A Formal Semantics for GOTO in the CProver Ecosystem. In: Ph.D. in Computer Science, University of Manchester, 2025 (Supervisor).
  2. Aldughaim, M. A. Interval Analysis and Methods in Software Analysis. In: Ph.D. in Computer Science, University of Manchester, 2025 (Supervisor).
  3. Matos Jr, J. B. P. An Automated Method for Neural Network Quantization Refinement. In: Ph.D. in Informatics, Federal University of Amazonas, 2025 (Supervisor).
  4. Song, X. Automated Verification and Repair of Quantized Neural Networks. In: Ph.D. in Computer Science, University of Manchester, 2024 (Co-Supervisor).
  5. Erdayandi, K. Privacy-Preserving Trading in Local Energy Markets. In: Ph.D. in Computer Science, University of Manchester, 2024 (Co-Supervisor).
  6. 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).
  7. 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).
  8. 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).
  9. Romero, M. J. Understanding the Microeconomic Impact of Automation in Digital Organisations. In: Ph.D. in Computer Science, University of Manchester, 2023 (Co-Supervisor).
  10. Trajanovski, T. Countering IoT Botnets. In: Ph.D. in Computer Science, University of Manchester, 2023 (Co-Supervisor).
  11. Thayaparan, M. Differentiable Constraint-based Solvers for Explanation-based Multi-hop Inference. In: Ph.D. in Computer Science, University of Manchester, 2023 (Co-Supervisor).
  12. Trindade, A. B. Automated Verification of Stand-alone Solar Photovoltaic Systems. In: D.Sc. in Informatics, Federal University of Amazonas, 2020 (Supervisor).
  13. 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. 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).
  2. 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).
  3. Hong. H. Verifying Quantized Neural Networks using SMT-Based Model Checking. In: M.Sc. in Advanced Computer Science, University of Manchester, 2023 (Supervisor).
  4. Li, x. Safety Verification of CUDA and Deep Neural Networks. In: M.Sc. in Advanced Computer Science, University of Manchester, 2023 (Supervisor).
  5. 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).
  6. 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).
  7. Salim, B. ESBMC-based Ethereum Smart Contract Security Verification. In: M.Sc. in Advanced Computer Science, University of Manchester, 2022 (Supervisor).
  8. Wu, C. Fuzzing a Software Verifier. In: M.Sc. in Advanced Computer Science, University of Manchester, 2022 (Supervisor).
  9. Li, M. Incremental Bounded Model Checking using Machine Learning Techniques. In: M.Sc. in Advanced Computer Science, University of Manchester, 2022 (Supervisor).
  10. Young, J. Verifying Binarised Neural Networks using SMT-Based Model Checking. In: M.Sc. in Advanced Computer Science, University of Manchester, 2022 (Supervisor).
  11. Lu, Y. Scaling up Bounded-Model-Checking for Internet of Things devices. In: M.Sc. in Advanced Computer Science, University of Manchester, 2022 (Supervisor).
  12. Sena, L. H. C. Automated Verification and Refutation of Quantized Neural Networks. In: M.Sc. in Electrical Engineering, Federal University of Amazonas, 2022 (Supervisor).
  13. He, H. Incremental Bounded Model Checking using Machine Learning Techniques. In: M.Sc. in Advanced Computer Science, University of Manchester, 2021 (Supervisor).
  14. 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).
  15. 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).
  16. Song, K. SMT-Based Bounded Model Checking for Solidity Smart Contracts. In: M.Sc. in Advanced Computer Science, University of Manchester, 2021 (Supervisor).
  17. Matulevicius, N. Verifying Information Flow Security for Blockchain-based Smart Contracts. In: M.Sc. in Advanced Computer Science, University of Manchester, 2021 (Supervisor).
  18. 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).
  19. Tan, V. L. Security Analyser Tool for Finding Vulnerabilities in Java Programs. In: M.Sc. in Advanced Computer Science, University of Manchester, 2020 (Supervisor).
  20. 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).
  21. 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).
  22. Alkhamissi, S. R. **Finding Software Vulnerabilities in Unmanned Aerial Vehicles. In: M.Sc. in Advanced Computer Science, University of Manchester, 2019 (Supervisor).
  23. 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).
  24. 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).
  25. 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).
  26. 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).
  27. 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).
  28. 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).
  29. 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).
  30. 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).
  31. 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).
  32. 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]
  33. 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).
  34. 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).