grants

Research funding secured as Principal or Co-Investigator, most recent first.

My research focuses on building software and AI systems that are safe, secure, and trustworthy. I create and deploy automated formal reasoning methods by combining SMT-based bounded model checking, symbolic execution, hybrid fuzzing, program synthesis, and machine learning. These approaches help identify vulnerabilities, verify critical safety features, and fix faulty code across embedded firmware, operating system kernels, IoT devices, smart contracts, CUDA programs, and quantized neural networks. My work supports open-source verification tools, especially ESBMC, which have won awards and ranked highly at the international competitions on software verification (SV-COMP) and testing (Test-Comp) at ETAPS.

  1. Combining Formal Methods with Large Language Models in ESBMC: Enabling Automated Program Verification through AI/ML, Amazon Research Award in Automated Reasoning, Amazon Science, 2026, USD 79,510 in unrestricted funds plus USD 40,000 in AWS promotional credits (I am the Principal Investigator).
  2. GenAIDE: Generative AI for Industrial Design Engineering, MSCA Doctoral Networks, European Commission – Horizon Europe (Ref. 101226927), 2025-2029, GBP 731,055 (or USD 928,440), funding two 48-month PhD studentships at the University of Manchester (I am the Principal Investigator).
  3. AI Trust in Complex Software: Requirements, Understanding, and Certification, BAE Systems, 2024-2025, GBP 300,000 (or USD 380,000), in collaboration with Dr. Youcheng Sun, Prof. Caroline Jay, and Dr. Suzanne Embury from the University of Manchester (UK) (I am the Co-Investigator and WP leader).
  4. Source Code Security with FuSeBMC-AI, Cyber security academic startup accelerator programme 2024-25 (phase 2), Innovate UK, 2024-2025, GBP 60,000 (or USD 75,000), in collaboration with Prof. Richard Allmendinger from the University of Manchester (UK) (I am the Co-Investigator and WP leader).
  5. Source Code Security with FuSeBMC-AI, Cyber security academic startup accelerator programme 2024-25 (phase 1), Innovate UK, 2024, GBP 31,500 (or USD 40,200), in collaboration with Prof. Richard Allmendinger from the University of Manchester (UK) (I am the Co-Investigator and WP leader).
  6. SECCOM: Securing composable hardware platforms, DSTL (Defence Science & Technology Laboratory), Engineering & Physical Sciences Research Council (EPSRC), 2023-2026, GBP 1,031,720 (or USD 1,313,271), in collaboration with Prof. John Goodacre and Dr. Bernardo Magri from the University of Manchester (UK) (I am the Co-Investigator and WP leader).
  7. SWPERFI: Artificial Intelligence Techniques for Software Performance Analysis and Optimization, Motorola Mobility, 2023-2025, BRL 4,492,346 (or USD 912,299), in collaboration with Dr. Rosiane de Freitas, Dr. Raimundo Barreto, and Dr. Vandermi Silva from the Federal University of Amazonas (Brazil) (I am the Co-Investigator and WP leader).
  8. AICodeRepair: Towards Self-Healing AI Code with Large Language Models and Formal Verification, GCHQ Government Communications Headquarters, 2023-2024, GBP 75,380 (or USD 93,156), in collaboration with Dr. Mustafa O. Mustafa from the University of Manchester (UK) (I am the Principal Investigator).
  9. Bounded Model Checking for Verifying and Testing Ethereum Consensus Specifications, Ethereum Foundation, 2023-2024, USD 114,680, in collaboration with Dr. Youcheng Sun from the University of Manchester (UK) (I am the Co-Investigator and WP leader).
  10. Using Artificial Intelligence/Machine Learning to assess source code in Escrow, UKRI Impact Acceleration Account, 2023-2024, GBP 86,339 (or USD 104,702) (I am the Principal Investigator).
  11. Develop and Evaluate a Model Checker Based Code Analysis Framework for Smart Contracts, LatticeX Foundation Ltd, 2022-2026, GBP 70,000 (or USD 86,560) (I am the Principal Investigator).
  12. Soteria - Demonstrating the Security Capabilities of the Morello System in the e-commerce Vertical Industrial Segment over the call for “ISCF digital security by design: technology enabled business-led demonstrator”, 2021-2024, GBP 2,647,375 (or USD 3,603,355), in collaboration with Prof. Mikel Lujan, Dr. Konstantin Korovin, Dr. Giles Reger, Dr. Christos Kotselidis, Dr. Elvira Uyarra, Dr. Richard Allmendinger, and Dr. Pierre Olivier from the University of Manchester (UK) (I am the Co-Investigator).
  13. ELEGANT: sEcure and seamLess EdGe-to-cloud ANalyTics, EU over the call for “Software Technologies”, 2021-2023, EUR 586,500 (or USD 687,084), in collaboration with Dr. Christos Kotselidis from the University of Manchester (UK) (I am the Co-Investigator).
  14. EnnCore: End-to-End Conceptual Guarding of Neural Architectures, EPSRC over the call for “Security for all in an AI-enabled society”, 2021-2024, GBP 2,151,950 (or USD 2,660,817), in collaboration with Prof. Gavin Brown, Prof. Mikel Lujan, Dr. Mustafa Mustafa, and Dr. Andre Freitas from the University of Manchester (UK) and Dr. Xiaowei Huang from the University of Liverpool (UK) (I am the Principal Investigator).
  15. SCorCH: Secure Code for Capability Hardware, EPSRC over the call for “ISCF Digital Security by Design”, 2020-2023, GBP 1,300,000 (or USD 1,627,593), in collaboration with Dr. Konstantin Korovin, Dr. Mustafa Mustafa, Dr. Pierre Olivier, and Dr. Giles Reger from the University of Manchester (UK) and Prof. Daniel Kroening from the University of Oxford (UK) (I am the Co-Investigator and WP leader).
  16. Formal Verification of Firmware, Intel Corporation, 2021-2024, GBP 66,000 (or USD 89,292) (I am the Principal Investigator).
  17. ARM Centre of Excellence at the University of Manchester, Arm Ltd., 2017-2021, GBP 250,000 (or USD 335,712), in collaboration with Prof. Gavin Brown, Prof. Mikel Lujan, and Dr. David Jackson (I am the Principal Investigator).
  18. Developing Critical Mass in Cybersecurity, UK Research and Innovation – Early Career Researchers, 2018-2020, GBP 65,108 (or USD 83,481), in collaboration with Dr. Giles Reger from the University of Manchester (UK) (I am the Principal Investigator).
  19. Counterexample-Guided Optimization Applied to the Daily Schedule of the Electrical Power Systems using Satisfiability Modulo Theories, National Centre for Scientific and Technological Development, 2018-2021, BRL 60,000 (or USD 15,114), in collaboration with Prof. Erlon Finardi from the Federal University of Santa Catarina (Brazil) (I am the Principal Investigator).
  20. Investigation and Development of Verification Algorithms of Embedded Software in Unmanned Aerial Vehicles using Machine Learning, Amazonas State Research Funding Agency, 2017-2018, BRL 87,400 (or USD 22,812), in collaboration with Prof. João Edgar Chaves Filho from the Federal University of Amazonas (Brazil) (I am the Co-Investigator and WP leader).
  21. Support for Scientific Production of the Research Group on Software and Systems Verification, Amazonas State Research Funding Agency, 2017-2018, BRL 16,992 (or USD 5,168) (I am the Principal Investigator).
  22. DSVerifier: A Bounded Model Checking Tool to Verify Digital Systems with Uncertainties, EPSRC Impact Acceleration Account, 2016-2017, GBP 8,462 (or USD 11,141), in collaboration with Prof. Daniel Kroening from the University of Oxford (UK) (I am the Co-Investigator and WP leader).
  23. Verification of C/C++ Programs Based on Multi-Core Processors, Nokia Institute of Technology, 2014-2016, BRL 451,231 (or USD 171,594) (I am the Principal Investigator).
  24. Hardware and Software Verification Based on Mathematical Induction for Embedded Systems, Amazonas State Research Funding Agency, 2014-2016, BRL 249,853 (or USD 95,014) (I am the Principal Investigator).
  25. SMT-based Bounded Model Checking of Multi-threaded Programs, British Council, 2014-2015, GBP 3,000 (or USD 4,554) (I am the Principal Investigator).
  26. Continuous Verification of C++ Programs Using SMT-based Bounded Model Checking, Nokia Institute of Technology, 2011-2013, BRL 287,631 (or USD 109,380) (I am the Principal Investigator).
  27. SMT-Based Bounded Model Checking Timed LTL Properties for Embedded Software, Royal Society International Exchange Grant, 2011-2013, GBP 11,600 (or USD 17,609), in collaboration with Prof. Bernd Fischer from the University of Southampton (UK) (I am the Co-Investigator).
  28. Verification of Temporal Properties in Embedded Software using Satisfiability Modulo Theories, National Centre for Scientific and Technological Development, 2013-2016, BRL 14,000 (or USD 5,324) (I am the Principal Investigator).
  29. Research and training of human resources, at undergraduate and graduate courses, in the areas of industrial automation, software development for mobile devices, and digital TV, Samsung / Institute of Development in Informatics, 2013-2016, BRL 7,190,550 (or USD 2,734,414), in collaboration with Dr. Cícero Costa, Dr. Marly Costa, Dr. João Chaves Filho, Dr. Vicente Lucena Jr., Dr. Andre Cavalcante, and Dr. Waldir Sabino Jr. from the Federal University of Amazonas (Brazil) (I am the Co-Investigator).