| Aug 17, 2026 |
Tong Wu passed his Ph.D. viva with minor corrections, defending the thesis Efficient Concurrent Software Verification with Bounded Model Checking and Deep Learning. The external examiner was Prof. Ajitha Rajan (University of Edinburgh) and the internal examiner Dr. Konstantin Korovin (University of Manchester); the thesis was supervised with Pavlos Petoumenos. Dr. Wu is the 14th Ph.D. student from our group to graduate in formal software verification, and works on our software verification spinout VeriBee.
|
| Aug 12, 2026 |
Two memory-safety vulnerabilities we found in the Base64 decoder of the AWS SDK for C++ using ESBMC have been assigned CVE-2026-19642 and CVE-2026-19643, and are fixed in v1.11.862. Joint work with Rafael Sá Menezes.
|
| Jul 01, 2026 |
Received an Amazon Research Award in Automated Reasoning (Fall 2025 cycle) for the project “Combining Formal Methods with Large Language Models in ESBMC: Enabling Automated Program Verification through AI/ML”.
|
| Jul 01, 2026 |
Our edited book Adversarial Example Detection and Mitigation Using Machine Learning (with Ehsan Nowroozi and Rahim Taheri) has been published by Springer Nature.
|
| Jun 24, 2026 |
Visited Minas Gerais, Brazil, between 15 and 24 June 2026. Gave the invited talk “From Research to Impact: Software Verification, Veribee, and Manchester–Brazil Opportunities” and a two-session formal verification workshop, built on our Software Security course, at the Universidade Federal de Itajubá (UNIFEI); presented collaboration perspectives on formal methods, software verification, and systems security for critical sectors at the Instituto Nacional de Telecomunicações (Inatel) and the Inatel Competence Center in Santa Rita do Sapucaí; and lectured on academic, scientific, and technological partnership opportunities with the UK at UNIFEI Pouso Alegre and Senac Pouso Alegre, with a class for SENAC Tech and UNIFEI Cybersecurity students.
|
| Apr 12, 2026 |
Gave the keynote talk “Cooperative AI-Assisted Formal Verification: Integrating LLMs with Model Checking for Scalable Software Assurance” at the 7th Workshop on Cooperative Software Verification (COOP 2026), co-located with ETAPS 2026, Turin, Italy.
|
| Apr 01, 2026 |
FuSeBMC, our white-box fuzzer for finding security vulnerabilities in programs, won three gold medals in the 8th Intl. Competition on Software Testing (Test-Comp 2026) at FASE’26. ESBMC, our SMT-based model checker for C/C++ programs, won one gold and one silver medal in the 15th Intl. Competition on Software Verification (SV-COMP 2026) at TACAS’26, ETAPS 2026, Turin, Italy.
|
| Nov 01, 2025 |
Local organiser of the CHERITech’25 conference, Manchester, UK.
|
| Oct 26, 2025 |
Gave the keynote talk “AI-Assisted Formal Verification: Towards Fast, Accessible, and Rigorous Software Verification” at the Generative Code Intelligence Workshop (GeCoIn 2025), co-located with ECAI 2025, Bologna, Italy.
|
| Jul 01, 2025 |
FuSeBMC won two gold and one silver medal at Test-Comp 2025, and ESBMC won two silver medals at SV-COMP 2025.
|
| Jul 01, 2025 |
Received an award in the contest for contributions of a new verification tool to the Verifying the Rust Standard Library project, Rust Foundation / Amazon Web Services.
|
| Jul 01, 2025 |
Started the project “GenAIDE: Generative AI for Industrial Design Engineering”, funded by the MSCA Doctoral Networks programme of the European Commission (Horizon Europe), 2025-2029, funding two PhD studentships at the University of Manchester.
|
| Oct 01, 2024 |
Our paper “LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling” received an ACM SIGSOFT Distinguished Paper Award at the 39th IEEE/ACM International Conference on Automated Software Engineering (ASE 2024).
|
| Jul 01, 2024 |
Started the projects “AI Trust in Complex Software: Requirements, Understanding, and Certification” with BAE Systems (2024-2025) and “Source Code Security with FuSeBMC-AI” with Innovate UK (2024-2025), in collaboration with Prof. Richard Allmendinger.
|
| Dec 01, 2023 |
Will start a project on “AICodeRepair: Towards Self-Healing AI Code with Large Language Models and Formal Verification” with the GCHQ Government Communications Headquarters, 2023-2024, in collaboration with Dr Mustafa Mustafa.
|
| Aug 01, 2022 |
Will start a project on “Using Artificial Intelligence/Machine Learning to assess source code in Escrow” with the UKRI/IAA, 2022-2023, in collaboration with Dr. Richard Allmendinger and Dr. Andre Freitas.
|
| Aug 01, 2022 |
Will start a project on “Bounded Model Checking for Verifying and Testing Ethereum Consensus Specifications” with the Ethereum Foundation, 2023-2024, in collaboration with Dr Youcheng Sun.
|
| Dec 01, 2021 |
FuSeBMC, our white-box fuzzer for finding security vulnerabilities in programs, won first place in the Cover-Error, Cover-Branches and Overall categories at Test-Comp 2022. JBMC, our verification tool for Java Bytecode, won second place in the Java overall category at SV-COMP 2022. ESBMC, our SMT-based model checker for C/C++ programs, has successfully participated at SV-COMP 2022. It got second place in three sub-categories, third in one sub-category, fourth in the ReachSafety category, seventh place among 40 state-of-the-art software verifiers at SV-COMP 2022!
|
| Jun 01, 2021 |
I became the new Director of the Arm Centre of Excellence at the University of Manchester.
|
| Dec 01, 2020 |
FuSeBMC, our white-box fuzzer for finding security vulnerabilities in programs, won first place in the Cover-Error category and second place in the Overall category at Test-Comp 2021. JBMC, our verification tool for Java Bytecode, won third place in the Java overall category at SV-COMP 2021. ESBMC, our SMT-based model checker for C/C++ programs, has successfully participated at SV-COMP 2021. It got first place in one sub-category, second place in four sub-categories, fourth place in the ReachSafety category, fifth place in the SoftwareSystems category. Overall, the sixth place among 25 state-of-the-art software verifiers at SV-COMP 2021!
|
| Nov 01, 2020 |
Will start a UKRI project on “Soteria - Demonstrating the Security Capabilities of the Morello System in the ecommerce Vertical Industrial Segment” over the call for ISCF digital security by design: technology enabled business-led demonstrator.
|
| Aug 01, 2020 |
Will start an EU project on “ELEGANT: sEcure and seamLess EdGe-to-cloud ANalyTics” over the call for Software Technologies.
|
| Jul 01, 2020 |
Will start an EPSRC project on “SCorCH: Secure Code for Capability Hardware” over the call for ISCF Digital Security by Design Research Projects.
|
| Feb 01, 2020 |
Will start an EPSRC project on “EnnCore: End-to-End Conceptual Guarding of Neural Architectures” over the call for Security for all in an AI enabled society.
|