7th Workshop on Cooperative Software Verification (COOP 2026)

Cooperative software verification aims to be more effective by bringing together different analysis methods. In this talk, I will introduce a new approach that integrates generative AI and formal verification. This approach is driven by the high costs of implementation bugs and the fact that large language models (LLMs) are not always reliable when used alone for software verification tasks. LLMs and formal methods work well together.

LLMs make it easier to understand and reason quickly about code and requirements, while model checking gives strong mathematical guarantees. To illustrate how this cooperation works, I will present ESBMC, a logic-based verification platform that supports different industrial programming languages (e.g., C, C++, Python, and Solidity), along with two AI-assisted verification workflows. First, LLMs create candidates for loop invariants, which ESBMC then formally checks. This enables scalable verification without the cost of loop unrolling. Second, SpecVerify turns natural-language requirements into formal properties. These are checked and improved through model checking, reaching over 79% logical equivalence with expert-written specifications. These workflows show how different tools can work together by sharing proof artifacts, combining various techniques, and using portfolio-style verification. Real-world case studies from industry show the practical benefits of cooperative AI-assisted verification.

Lucas C. Cordeiro is a Full Professor of Computer Science at the University of Manchester, where he leads the Systems and Software Security (S3) Research Group and serves as Business Engagement and Innovation Director. He also directs the Arm Centre of Excellence and is affiliated with postgraduate programs at the Federal University of Amazonas. Beyond academia, he is Chief Scientific Officer at VeriBee and a technical advisory board member at Axiomise.

His previous roles include postdoctoral researcher at the University of Oxford, research engineer at Diffblue, and software engineering positions at Siemens/BenQ Mobile and NXP Semiconductors. His research focuses on software model checking, automated testing, program synthesis, security, and cyber-physical systems. He has co-authored 180+ peer-reviewed papers, received major awards, including the Most Influential Paper at ASE 2023 and the Distinguished Paper Awards at ICSE 2011 and ASE 2024, won numerous international competition prizes, and secured over USD 13 million in research funding.