CV

Education, appointments, awards, research grants, supervision and teaching. The full curriculum vitae is available as a PDF.

Contact Information

Name Lucas C. Cordeiro
Professional Title Full Professor of Computer Science, University of Manchester
Email lucas.cordeiro@manchester.ac.uk

Professional Summary

Software engineering, formal methods, automated program verification and synthesis, software testing, security, and embedded and cyber-physical systems. Leads the Systems and Software Security (S3) Research Group and directs the Arm Centre of Excellence at the University of Manchester.

Experience

  • 2025 - present

    Manchester, UK

    Scientific Lead Advisor
    ByteRepair
    • University of Manchester spinout applying formal verification to automated code security analysis and repair.
  • 2018 - present

    Manchester, UK

    Full Professor
    University of Manchester
    • Director of Business Engagement and Innovation, Department of Computer Science.
    • Director of the Arm Centre of Excellence.
    • Leader of the Systems and Software Security (S3) Research Group.
    • Leader of the Software Security and Automated Reasoning theme in the Advanced Computer Science MSc programme.
    • Member of the EPSRC Peer Review Full College.
  • 2009 - present

    Manaus, Brazil

    Associate Professor
    Federal University of Amazonas
    • Permanent member of the postgraduate programmes in Electrical Engineering (PPGEE) and Informatics (PPGI).
    • Leader of the Systems and Software Verification Research Group.
    • Course Leader of Electrical Engineering, 2011-2015.
  • 2022 - 2023

    Abu Dhabi, UAE

    Consultant and Advisor, Digital Security Unit
    Technology Innovation Institute (TII)
    • Advised the Digital Security Unit’s research programmes, strategy and roadmap.
  • 2016 - 2018

    Oxford, UK

    Researcher / Research Engineer
    University of Oxford / Diffblue
    • Extended the CProver framework to support exception handling and the Java standard libraries.
    • Implemented components of the CounterExample Guided Inductive Synthesis (CEGIS) framework.
    • Built tools to synthesise, verify and validate digital control systems with uncertainties.
  • 2007 - 2008

    Manaus, Brazil

    Set-top Box Software Engineer
    R&D Center for the Industrial Pole of Manaus (CT-PIM) / NXP
    • Linux drivers for ISDB-T, DVB-T and DVB-S2 tuner and demodulator silicon.
    • Automated unit and functional tests for Linux device drivers.
  • 2005 - 2007

    Manaus, Brazil

    Software Engineer
    BenQ-Siemens Eletroeletronica S.A.
    • Requirements, planning and tracking for the linuX Mobile Phone Manager (XMPM).
    • Configuration, change, build and release management for Siemens mobile phone generations 75 and 85.

Education

  • Southampton, UK

    PhD
    University of Southampton
    Computer Science
    • Thesis: SMT-Based Bounded Model Checking of Multi-threaded Software in Embedded Systems.
    • Supervisor: Prof. Bernd Fischer. ORSAS/ECS scholarship holder.

  • Manaus, Brazil

    MSc
    Federal University of Amazonas
    Informatics
    • Dissertation: An Agile HW/SW Development Methodology for Embedded Systems.
    • Supervisor: Prof. Raimundo S. Barreto.

  • Manaus, Brazil

    BSc
    Federal University of Amazonas
    Electrical Engineering
    • Project: Developing Real-Time Applications with LEGO Mindstorms.
    • CAPES/DAAD scholarship at the University of Stuttgart, Germany, 2003-2004.

Awards

  • 2026
    Amazon Science

    For the project “Combining Formal Methods with Large Language Models in ESBMC: Enabling Automated Program Verification through AI/ML” (Fall 2025 cycle).

  • 2012
    SV-COMP and Test-Comp, held with ETAPS

    Gold, silver and bronze medals across fifteen editions of SV-COMP and eight of Test-Comp, for ESBMC, FuSeBMC, JBMC, DepthK and Map2Check. Most recently three gold medals at Test-Comp 2026 and one gold and one silver at SV-COMP 2026.

  • 2024
    39th IEEE/ACM International Conference on Automated Software Engineering (ASE)

    For “LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling”.

  • 2023
    38th IEEE/ACM International Conference on Automated Software Engineering (ASE)

    Recognising the lasting impact of our work on SMT-based bounded model checking.

  • 2023
    23rd Brazilian Symposium on Information and Computational Systems Security (SBSeg)
  • 2025
    Rust Foundation / Amazon Web Services

    For a contribution to the Verifying the Rust Standard Library project.

  • 2011
    33rd International Conference on Software Engineering (ICSE)
  • 2015
    V Brazilian Symposium on Computing Systems Engineering (SBESC)
  • 2008
    23rd ACM Symposium on Applied Computing, Real-Time Systems track (SAC)

Research grants

Combining Formal Methods with Large Language Models in ESBMC: Amazon Research Award in Automated Reasoning, 2026. USD 79,510 unrestricted plus USD 40,000 in AWS credits. Principal Investigator.
GenAIDE: Generative AI for Industrial Design Engineering: MSCA Doctoral Networks, European Commission Horizon Europe, 2025-2029. GBP 731,055, funding two PhD studentships at Manchester. Principal Investigator.
AI Trust in Complex Software: Requirements, Understanding and Certification: BAE Systems, 2024-2025. GBP 300,000. Co-Investigator and work package leader.
Source Code Security with FuSeBMC-AI: Innovate UK cyber security academic startup accelerator, 2024-2025. GBP 91,500 across two phases. Co-Investigator and work package leader.
SECCOM: Securing composable hardware platforms: DSTL and EPSRC, 2023-2026. GBP 1,031,720. Co-Investigator and work package leader.
SWPERFI: AI techniques for software performance analysis and optimisation: Motorola Mobility, 2023-2025. BRL 4,492,346. Co-Investigator and work package leader.
EnnCore: End-to-End Conceptual Guarding of Neural Architectures: EPSRC, 2021-2024. GBP 2,151,950. Principal Investigator.
SCorCH: Secure Code for Capability Hardware: EPSRC, 2020-2023. GBP 1,300,000. Co-Investigator and work package leader.
Soteria - Security Capabilities of the Morello System: ISCF Digital Security by Design demonstrator, 2021-2024. GBP 2,647,375. Co-Investigator.
Career total: Over USD 16.4M 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. Full list in the CV PDF.

Supervision

Doctoral: 13 PhD theses completed and four in progress, on bounded model checking, hybrid fuzzing, neural network verification and repair, and privacy-preserving distributed learning.
Masters and undergraduate: 3 MPhil dissertations, 30 MSc dissertations, 30 final year projects, 6 scientific initiations and 10 internships.
External PhD examination: External examiner for 13 PhD candidates at Manchester, Bristol, Edinburgh, Essex, Lancaster, UWE, IIT Kanpur, Gran Sasso Science Institute, USP and UFAM.

Teaching

Software Security: University of Manchester, graduate, since 2020 (40+ students).
Algorithms and Data Structures: University of Manchester, undergraduate, since 2020 (300+ students).
Algorithms and Imperative Programming: University of Manchester, undergraduate, 2018-2019 (280+ students).
Verification of Software and Systems: Federal University of Amazonas, graduate, since 2021 and 2014-2016.
Real-Time Systems and Real-Time Programming: Federal University of Amazonas, graduate and undergraduate, 2011-2015 and since 2021.

Tools

ESBMC: Efficient SMT-based Context-Bounded Model Checker for C, C++, CUDA, Python and Solidity. Award-winning at SV-COMP and Test-Comp since 2012.
FuSeBMC: White-box fuzzer combining bounded model checking, fuzzing and static analysis for test generation.
DSVerifier: Bounded model checker for digital systems with finite word length effects.
JBMC and Map2Check: Bounded model checking for Java bytecode, and unit test generation and memory safety checking for C.

Languages

Portuguese : Native
English : Native standard
German : High-school level