| Oct 30 |
New blog post: “LLMs propose, verifiers check”, on how our group has combined large language models with model checking, SMT solving and theorem proving since 2023, and on three open challenges that neither academia nor industry can solve alone.
|
| Oct 23 |
Welcome to Manan Mal and Mohd Ruhul Ameen, who have joined our group at The University of Manchester as doctoral candidates in GenAIDE, the Generative AI for Industrial Design Engineering Marie Skłodowska-Curie Actions Industrial Doctoral Network funded under Horizon Europe. Manan (DC7) works on robust code generation for simulation and optimization, and Ruhul (DC8) on LLM-based self-repair of simulation and optimization software; both projects extend ESBMC, so that one checks what the model generates and the other repairs it (slides).
|
| Oct 16 |
Gave the invited talk “Formal Verification of LLM-Generated Code” at FATTW 2026, the invitation-only workshop on the new foundations of software testing co-located with ASE 2026 in Munich, Germany, on how formal verification can check the code that large language models generate.
|
| Oct 01 |
An uncontrolled-recursion vulnerability we found in the Ion reader of Amazon Ion Python using ESBMC has been assigned CVE-2026-104020 (GHSA-93q6-f8hx-vv7f), and is fixed in v0.15.0. Joint work with Weiqi Wang.
|
| Sep 18 |
Gave the invited talk “Verifying What Generative AI Builds: Formal Methods for the AI Partner in Engineering” for GenAIDE, the Generative AI for Industrial Design Engineering Marie Skłodowska-Curie Actions Industrial Doctoral Network funded under Horizon Europe, at The University of Manchester, setting out how formal methods can check what generative models produce when AI becomes a partner in the design and engineering loop.
|
| Sep 09 |
Gave the talk “Verifiable, Trustworthy Software and Secure Networked Systems” to BT Group at a business engagement event at The University of Manchester, setting out the Systems and Software Security (S3) group’s capability across software verification, AI assurance, post-quantum cryptography and networked-systems security, together with engagement routes and the talent pipeline.
|
| Aug 25 |
Our paper “A Simulation Study of Cost-Aware Paradigms for Enterprise Distributed Agents with DAF” received a Best Paper Award in the Smart Computing Frontier track of the 2026 International Conference on Web Services (ICWS 2026), Kuala Lumpur, Malaysia. Joint work with Huan Chen, Jian Jin, Pan Ren, Xiang Song and Liang-Jie Zhang.
|
| Aug 17 |
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 |
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 |
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 |
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 |
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 |
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 |
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.
|
