Lucas C. Cordeiro
Full Professor of Computer Science, University of Manchester. Director, Arm Centre of Excellence.
Department of Computer Science
Kilburn Building, Oxford Road
Manchester M13 9PL, UK
Lucas C. Cordeiro is a Full Professor in the Department of Computer Science (CS) at the University of Manchester (UoM), where he leads the Systems and Software Security (S3) Research Group. Prof. Cordeiro is also the Business Engagement and Innovation Director in the CS department and the Arm Centre of Excellence Director at UoM. In addition, he is affiliated with the Trusted Digital Systems Cluster at the Centre for Digital Trust and Society, the Formal Methods Group at UoM, and the Post-Graduate Programs in Electrical Engineering (PPGEE) and Informatics (PPGI) at the Federal University of Amazonas, Brazil. He is the Chief Technology Officer at VeriBee, a spinout from the University of Manchester that aims to revolutionize the software testing/verification market; he is the Scientific Lead Advisor at ByteRepair, a University of Manchester spinout applying formal verification to automated code security analysis and repair, and a member of the technical advisory board at Axiomise. Before joining the University of Manchester, he worked as a post-doctoral researcher at the University of Oxford and as a research engineer at Diffblue. In addition, Dr. Cordeiro worked for five years as a software engineer at Siemens / BenQ Mobile and CTPIM / NXP semiconductors. He also leads the Software Security and Automated Reasoning theme in the Advanced Computer Science MSc programme at UoM. His work focuses on software model checking, automated testing, program synthesis, software security, embedded and cyber-physical systems, and, more recently, on combining formal methods with large language models. He has co-authored more than 200 peer-reviewed publications in the most prestigious venues (e.g., ICSE, CAV, TACAS, FSE, ASE, ISSTA, TSE, TR, TC), comprising 45 journal articles, 156 conference and workshop papers, one edited book, and four book chapters, with an h-index of 37. He has received various international awards, including an Amazon Research Award in Automated Reasoning (Fall 2025), the Most Influential Paper Award at ASE’23, ACM SIGSOFT Distinguished Paper Awards at ICSE’11 and ASE’24, the Best Tool Paper Award at SBSeg’23, best paper awards at SBESC’15 and SAC’08, and 56 medals from the international competitions on software verification (SV-COMP) and testing (Test-Comp) from 2012 to 2026. He has a proven track record of securing research funding from Amazon, BAE Systems, British Council, CNPq, EPSRC, the European Commission, FAPEAM, GCHQ, Innovate UK, Intel, Motorola, Nokia Institute of Technology, the Royal Society, Samsung, and UKRI (career total over USD 16.4M). He has supervised 14 PhD theses, three MPhil dissertations, and 35 MSc dissertations, and has acted as an external PhD examiner for 14 candidates at the universities of Manchester, Bristol, Edinburgh, Essex, Lancaster and the West of England in the UK, IIT Kanpur in India, the Gran Sasso Science Institute and Ca’ Foscari University of Venice in Italy, and the federal universities of Amazonas and Minas Gerais and the University of São Paulo in Brazil. Full CV
His publication list is also indexed by DBLP, the ACM Author Profile, SCOPUS, Web of Science and Google Scholar.
news
| Oct 30, 2026 | 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, 2026 | 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, 2026 | 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, 2026 | 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, 2026 | 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. |