pith. sign in

arxiv: 2605.26169 · v2 · pith:WGCWXNJOnew · submitted 2026-05-25 · 💻 cs.SE · cs.LO

ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification

Pierre Dantas , Lucas Cordeiro , Waldir Junior This is my paper

Pith reviewed 2026-06-29 21:07 UTC · model grok-4.3

classification 💻 cs.SE cs.LO
keywords ESBMCformal verificationmodel checkingSMT solverssoftware verificationLLM integrationagentic architectureindustrial deployment
0
0 comments X

The pith

ESBMC has grown from a research prototype for embedded C into an industrially deployed autonomous verification platform integrated with LLMs and AI agents.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper traces ESBMC's development since 2009, documenting expansions in verification techniques, support for nine languages, integration of industrial SMT solvers, and recent couplings with large language models and autonomous agents. This trajectory establishes the tool as a natively autonomous verification kernel capable of self-directed model checking. A sympathetic reader would care because the survey shows how one research effort scaled to handle complex software correctness tasks with documented competition success and real-world use. The account also covers funding totals, peer awards, a spin-off, and a defense deployment to illustrate economic and practical reach. It ends by outlining open problems in scalability, neurosymbolic methods, and sustainability.

Core claim

The survey establishes that ESBMC has transformed from its original design for verifying embedded ANSI-C software into one of the most versatile and industrially capable formal verification platforms, achieving the first industrial deployment of an integrated agentic model-checking architecture and thereby operating as a natively autonomous verification kernel rather than a passive backend. The account records 43 awards at SV-COMP and Test-Comp, distinguished paper recognitions, over GBP 9.3 million and EUR 4.98 million in public funding, and its role as a backend for LLM-driven self-healing software and loop invariant generation.

What carries the argument

ESBMC, the Efficient SMT-Based Context-Bounded Model Checker, which carries the argument through its successive expansions in language front-ends, solver integrations, and couplings to large language models and autonomous agent architectures.

If this is right

  • Further language front-ends could enable cross-language verification tasks without separate tools.
  • LLM couplings already support self-healing code and invariant generation as direct applications.
  • The agentic architecture shifts verification from reactive checking to proactive, self-directed exploration.
  • Addressing the listed challenges in scalability and counterexample intelligibility would widen practical adoption.
  • Sustainability of the open-source effort directly affects continued industrial uptake.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar verification tools could adopt agent-based control loops to reduce manual configuration overhead.
  • The documented funding and deployment pattern offers a template for moving other academic model checkers toward industrial use.
  • Improvements in counterexample presentation might allow non-experts to act on verification results more quickly.
  • Neurosymbolic extensions could combine the existing SMT core with learned heuristics for larger state spaces.

Load-bearing premise

The narrative of steady growth and impact rests on the premise that the cited awards, funding figures, spin-off, and industrial deployments accurately reflect the tool's record without major selection bias or omission.

What would settle it

Evidence that the reported competition awards or industrial deployments have been substantially overstated or that the agentic architecture has not achieved autonomous operation in practice would undermine the central claim of maturation into an industrially capable autonomous kernel.

Figures

Figures reproduced from arXiv: 2605.26169 by Lucas Cordeiro, Pierre Dantas, Waldir Junior.

Figure 1
Figure 1. Figure 1: PRISMA-style search and selection flow. Combined primary and supplementary searches across arXiv, [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Chronological milestones of ESBMC major releases from its first publication at ASE 2009 through version 7.7 [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Architecture of ESBMC’s SMT back-end. A source program in any supported language (C, C [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Overview of k-induction in ESBMC. The base case unrolls execution for k steps and checks ¬P is unsatisfiable, ruling out counterexamples of length ≤k. The inductive step assumes P holds for k consecutive states and proves it at state k+1; UNSAT closes the proof for all lengths. When the inductive step fails (SAT), the hypothesis is too weak and is strengthened by one of two sources: static interval analysi… view at source ↗
Figure 5
Figure 5. Figure 5: Cumulative growth of language support in ESBMC (2009–2025). Each step corresponds to the introduction of [PITH_FULL_IMAGE:figures/full_fig_p012_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Annual awards obtained by ESBMC at SV-COMP (diagonal hatching) and Test-Comp (dotted) from 2012 to [PITH_FULL_IMAGE:figures/full_fig_p015_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: ESBMC verification pipeline. Source programs are parsed by language-specific front-ends into a common [PITH_FULL_IMAGE:figures/full_fig_p016_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Chronological milestones of ESBMC’s AI and LLM integration (2023–2025). Key contributions include the [PITH_FULL_IMAGE:figures/full_fig_p018_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Repair success rate achieved by the ESBMC-AI framework [ [PITH_FULL_IMAGE:figures/full_fig_p019_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: LLM-assisted loop invariant generation pipeline. The LLM proposes candidate invariants from the loop [PITH_FULL_IMAGE:figures/full_fig_p020_10.png] view at source ↗
read the original abstract

The Efficient SMT-Based Context-Bounded Model Checker (ESBMC) has grown from a research prototype for verifying embedded ANSI-C software into one of the most versatile and industrially capable formal verification platforms available today. Since its first publication in 2009, ESBMC has undergone persistent evolution: expanding its verification techniques, widening its language support to nine front-ends, integrating industrial-strength SMT solvers, and - most recently - coupling with Large Language Models (LLMs) and autonomous AI agents. This survey traces the full trajectory of ESBMC from its original design principles to the state of the art in 2025-2026, documenting 43 awards at SV-COMP and Test-Comp, peer recognition at leading software engineering venues, including a Distinguished Paper Awards at ICSE'11 and ASE'24, a Most Influential Paper Award at ASE'23, and a Best Tool Paper Award at SBSeg'23, its role as a formal verification backend for LLM-driven self-healing software and loop invariant generation, and the first industrial deployment of an integrated agentic model-checking architecture through the NVIDIA-OpenSMA framework, establishing ESBMC as a natively autonomous verification kernel rather than a passive validation backend. We synthesize its economic impact - over GBP 9.3 million and EUR 4.98 million in confirmed public research funding, the VeriBee spin-off, and a defense industrial deployment at Lockheed Martin - and conclude with a structured agenda of open challenges spanning scalability, neurosymbolic verification, counterexample intelligibility, cross-language verification, safety standards compliance, and open-source sustainability.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims that ESBMC has evolved since 2009 from a research prototype for embedded ANSI-C verification into one of the most versatile and industrially capable formal verification platforms, with expansions to nine language front-ends, SMT solver integrations, LLM and autonomous AI agent couplings, 43 SV-COMP/Test-Comp awards, peer recognitions including Distinguished Paper Awards, over GBP 9.3M and EUR 4.98M in funding, a VeriBee spin-off, industrial deployments at Lockheed Martin and the first agentic model-checking architecture via NVIDIA-OpenSMA, and concludes with an agenda of open challenges in scalability, neurosymbolic verification, and related areas.

Significance. If the documented trajectory, awards, funding, and deployments hold, the survey is significant as a comprehensive case study of how formal verification tools have matured and integrated with AI techniques, offering concrete evidence of industrial adoption and economic impact that can guide future work on autonomous and self-healing systems. The explicit future agenda also contributes by identifying actionable open problems for the field.

major comments (2)
  1. [Abstract] Abstract: The assertion of 'the first industrial deployment of an integrated agentic model-checking architecture through the NVIDIA-OpenSMA framework' is load-bearing for the central claim that ESBMC is now a 'natively autonomous verification kernel rather than a passive validation backend'. This requires explicit comparison to prior LLM/agent-integrated verification efforts in the literature to substantiate the primacy claim and address risks of incomplete synthesis in the impact narrative.
  2. [Abstract] Abstract: The synthesis of economic impact via 43 awards, >GBP 9.3 million and EUR 4.98 million funding, and specific deployments underpins the trajectory assessment. The paper should detail the aggregation methodology and source verification for these figures (e.g., in a dedicated methods subsection) to confirm completeness and mitigate selection bias concerns for the overall narrative.
minor comments (2)
  1. [Abstract] Abstract: The subjective phrasing 'one of the most versatile and industrially capable' would benefit from qualification via comparative metrics against peer tools.
  2. The list of awards, funding sources, and deployments should be cross-referenced to a consolidated table or appendix for improved readability and traceability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments, which help strengthen the survey's claims on ESBMC's trajectory and impact. We address each major comment below and commit to revisions that enhance transparency and substantiation without altering the documented facts.

read point-by-point responses

  1. Referee: [Abstract] The assertion of 'the first industrial deployment of an integrated agentic model-checking architecture through the NVIDIA-OpenSMA framework' is load-bearing for the central claim that ESBMC is now a 'natively autonomous verification kernel rather than a passive validation backend'. This requires explicit comparison to prior LLM/agent-integrated verification efforts in the literature to substantiate the primacy claim and address risks of incomplete synthesis in the impact narrative.

    Authors: We agree that the 'first' claim benefits from explicit substantiation. The manuscript's positioning draws from the authors' synthesis of the literature up to 2025-2026, where no prior work describes an integrated agentic architecture deployed industrially via a framework like NVIDIA-OpenSMA. To address the concern directly, we will revise the abstract and add a concise comparative paragraph in Section 5 (or a new subsection) contrasting ESBMC+OpenSMA with prior efforts such as LLM-based invariant generation in other tools, agentic loops in research prototypes, and non-industrial AI couplings. This will clarify the novelty of the industrial integration while preserving the narrative. revision: yes

  2. Referee: [Abstract] The synthesis of economic impact via 43 awards, >GBP 9.3 million and EUR 4.98 million funding, and specific deployments underpins the trajectory assessment. The paper should detail the aggregation methodology and source verification for these figures (e.g., in a dedicated methods subsection) to confirm completeness and mitigate selection bias concerns for the overall narrative.

    Authors: We concur that methodological transparency is essential for the funding, awards, and deployment figures. The numbers derive from verifiable public sources (SV-COMP/Test-Comp archives, UKRI/EU funding databases, project reports, and direct confirmations from partners like Lockheed Martin and VeriBee), but the current manuscript does not detail the compilation process. We will add a dedicated 'Data Sources and Aggregation Methodology' subsection early in the paper (e.g., after the introduction) that enumerates the sources, inclusion criteria, cross-verification steps, and any limitations to mitigate selection bias concerns. revision: yes

Circularity Check

0 steps flagged

No circularity: survey is factual historical synthesis without derivations or predictions

full rationale

This is a survey paper with no equations, no fitted parameters, no predictions, and no derivation chain. The narrative recounts ESBMC's history via citations to prior publications, awards, and deployments. No step reduces a claimed result to its own inputs by construction, self-definition, or load-bearing self-citation of unverified theorems. Self-citations are expected in a tool survey and do not create circularity under the rules, as the cited results are external publications rather than internal fits renamed as predictions. The paper is self-contained as a literature synthesis.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

As a survey paper, there are no free parameters, axioms, or invented entities introduced in support of new claims. The content rests on standard practices of literature review and citation of prior publications.

pith-pipeline@v0.9.1-grok · 5826 in / 1233 out tokens · 37657 ms · 2026-06-29T21:07:57.472046+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

110 extracted references · 60 canonical work pages

  1. [1]

    John Hatcliff, Andrew King, Insup Lee, Alasdair Macdonald, Anura Fernando, Michael Robkin, Eugene Vasserman, Sandy Weininger, and Julian M. Goldman. Rationale and Architecture Principles for Medical Application Platforms. In2012 IEEE/ACM Third International Conference on Cyber-Physical Systems, page 3–12, Beijing, China, April 2012. IEEE. doi: 10.1109/icc...

    work page doi:10.1109/iccps.2012.9 2012

  2. [2]

    Dennis, Clare Dixon, and Michael Fisher

    Matt Luckcuck, Marie Farrell, Louise A. Dennis, Clare Dixon, and Michael Fisher. Formal Specification and Verification of Autonomous Robotic Systems: A Survey.ACM Computing Surveys, 52(5):1–41, September 2019. ISSN 1557-7341. doi: 10.1145/3342355

    work page doi:10.1145/3342355 2019

  3. [3]

    de Lima Filho, and Lucas C

    Kunjian Song, Nedas Matulevicius, Eddie B. de Lima Filho, and Lucas C. Cordeiro. Esbmc-solidity: an smt-based model checker for solidity smart contracts. InProceedings of the ACM/IEEE 44th International Conference on Software Engineering: Companion Proceedings, ICSE ’22, page 65–69, Pittsburgh, PA, USA, May 2022. ACM. doi: 10.1145/3510454.3516855

    work page doi:10.1145/3510454.3516855 2022

  4. [4]

    Formal Methods: Practice and Experience.ACM Computing Surveys, 41(4):1–36, October 2009

    Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald. Formal Methods: Practice and Experience.ACM Computing Surveys, 41(4):1–36, October 2009. ISSN 1557-7341. doi: 10.1145/1592434. 1592436

    work page doi:10.1145/1592434 2009

  5. [5]

    Clarke, Thomas A

    Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem.Handbook of Model Checking. Springer International Publishing, Cham, Switzerland, 2018. ISBN 9783319105758. doi: 10.1007/978-3-319-10575-8

    work page doi:10.1007/978-3-319-10575-8 2018

  6. [6]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 1999

    Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu.Symbolic Model Checking without BDDs, page 193–207. Springer Berlin Heidelberg, Berlin, Heidelberg, 1999. ISBN 9783540490593. doi: 10.1007/3-540-49059-0_14

    work page doi:10.1007/3-540-49059-0_14 1999

  7. [7]

    Spectral Deferred Correction Methods for Ordinary Differential Equations

    Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded Model Checking Using Satisfiability Solving.Formal Methods in System Design, 19(1):7–34, July 2001. ISSN 1572-8102. doi: 10.1023/a: 1011276507260

    work page doi:10.1023/a: 2001

  8. [8]

    SMT-Based Bounded Model Checking for Embedded ANSI-C Software.IEEE Transactions on Software Engineering, 38(4):957–974, July 2012

    Lucas Cordeiro, Bernd Fischer, and Joao Marques-Silva. SMT-Based Bounded Model Checking for Embedded ANSI-C Software.IEEE Transactions on Software Engineering, 38(4):957–974, July 2012. ISSN 0098-5589. doi: 10.1109/tse.2011.59

    work page doi:10.1109/tse.2011.59 2012

  9. [9]

    Gadelha, Felipe R

    Mikhail R. Gadelha, Felipe R. Monteiro, Jeremy Morse, Lucas C. Cordeiro, Bernd Fischer, and Denis A. Nicole. ESBMC 5.0: an Industrial-Strength C Model Checker. InProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ASE’18, page 888–891, Manchester, UK, September 2018. ACM. doi: 10.1145/3238147.3240481

    work page doi:10.1145/3238147.3240481 2018

  10. [10]

    Gadelha, Franz Brauße, Rafael S

    Kunjian Song, Mikhail R. Gadelha, Franz Brauße, Rafael S. Menezes, and Lucas C. Cordeiro.ESBMC v7.3: Model Checking C++ Programs Using Clang AST, page 141–152. Springer Nature Switzerland, Cham, Switzerland, December 2023. ISBN 9783031493423. doi: 10.1007/978-3-031-49342-3_9

    work page doi:10.1007/978-3-031-49342-3_9 2023

  11. [11]

    Springer Nature Switzerland, Luxembourg City, Luxembourg, 2024

    Rafael Sá Menezes, Mohannad Aldughaim, Farias, et al.ESBMC v7.4: Harnessing the Power of Intervals: (Competition Contribution), page 376–380. Springer Nature Switzerland, Luxembourg City, Luxembourg, 2024. ISBN 9783031572562. doi: 10.1007/978-3-031-57256-2_24

    work page doi:10.1007/978-3-031-57256-2_24 2024

  12. [12]

    ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction

    Rafael Menezes et al. ESBMC v7.7: Efficient Concurrent Software Verification with Scheduling, Incremental SMT and Partial Order Reduction. InProceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025), Lecture Notes in Computer Science, Hamilton, New Zealand, 2025. Springer. doi: 10.10...

    work page doi:10.1007/978-3-031-90660-2_16 2025

  13. [13]

    Competition on Software Verification (SV-COMP)

    Dirk Beyer. Competition on Software Verification (SV-COMP). InProceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), volume 36 ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification 7214 ofLecture Notes in Computer Science, pages 504–...

    2012

  14. [14]

    Springer Nature Switzerland, Luxembourg City, Luxembourg, 2024

    Dirk Beyer.State of the Art in Software Verification and Witness Validation: SV-COMP 2024, page 299–329. Springer Nature Switzerland, Luxembourg City, Luxembourg, 2024. ISBN 9783031572562. doi: 10.1007/ 978-3-031-57256-2_15

    2024

  15. [15]

    ESBMC: An Industrial-Strength C Model Checker - Competition Results

    SSVLab. ESBMC: An Industrial-Strength C Model Checker - Competition Results. https://ssvlab.github. io/esbmc/sv-comp.html, 2024. Accessed: May 2026

    2024

  16. [16]

    Monteiro, Mikhail R

    Felipe R. Monteiro, Mikhail R. Gadelha, and Lucas C. Cordeiro. Model Checking C++ Programs.Software Testing, Verification and Reliability, 32(1):e1793, September 2021. ISSN 1099-1689. doi: 10.1002/stvr.1793

    work page doi:10.1002/stvr.1793 2021

  17. [17]

    Farias, Rafael Menezes, and Lucas C

    Felipe R. Farias, Rafael Menezes, and Lucas C. Cordeiro. ESBMC-Python: A Bounded Model Checker for Python Programs. InProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2024), Vienna, Austria, 2024. ACM. doi: 10.1145/3650212.3685304

    work page doi:10.1145/3650212.3685304 2024

  18. [18]

    Expanding the Rust Formal Verification Ecosys- tem: Welcoming ESBMC

    Rust Foundation. Expanding the Rust Formal Verification Ecosys- tem: Welcoming ESBMC. https://rustfoundation.org/media/ expanding-the-rust-formal-verification-ecosystem-welcoming-esbmc/ , 2024. Accessed: May 2026

    2024

  19. [19]

    Cordeiro

    Norbert Tihanyi, Yiannis Charalambous, Ridhi Jain, Mohamed Amine Ferrag, and Lucas C. Cordeiro. A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification. In2025 IEEE/ACM International Conference on Automation of Software Test (AST), pages 136–147, Ottawa, ON, Canada, apr 28 2025. IEEE, IEEE. doi: 10.1...

    work page doi:10.1109/ast66626.2025.00020 2025

  20. [20]

    Cordeiro

    Yiannis Charalambous, Edoardo Manino, and Lucas C. Cordeiro. Automated Repair of AI Code with Large Language Models and Formal Verification, 2024

    2024

  21. [21]

    Muhammad A. A. Pirzada, Giles Reger, Ahmed Bhayat, and Lucas C. Cordeiro. LLM-Generated Invariants for Bounded Model Checking Without Loop Unrolling. InProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, pages 1395–1407, Sacramento, CA, USA, oct 27 2024. ACM, ACM. doi: 10.1145/3691620.3695512

    work page doi:10.1145/3691620.3695512 2024

  22. [22]

    Cordeiro, and Liping Zhao

    Weiqi Wang, Marie Farrell, Lucas C. Cordeiro, and Liping Zhao. Supporting software formal verification with large language models: An experimental study. In2025 IEEE 33rd International Requirements Engineering Conference (RE), page 423–431, Reykjavik, Iceland, September 2025. IEEE. doi: 10.1109/re63999.2025.00049

    work page doi:10.1109/re63999.2025.00049 2025

  23. [23]

    Agentic model checking, 2026

    Youcheng Sun, Jiawen Liu, Daniel Kroening, and Jason Xue. Agentic model checking, 2026

    2026

  24. [24]

    Add ESBMC verification harnesses for OpenSMA

    Alan Cheng and Lucas C. Cordeiro. NVIDIA-OpenSMA: ESBMC verification harnesses for OpenSMA (vr_sma branch). https://github.com/lucasccordeiro/NVIDIAOpenSMA/commits/vr_sma/, 2025. Repository initialised 30 July 2025 (commit 0dcdcd1); first verification commit 9b8e1a4 (“Add ESBMC verification harnesses for OpenSMA”), April 2026

    2025

  25. [25]

    Guidelines for Performing Systematic Literature Reviews in Software Engineering

    Barbara Kitchenham and Stuart Charters. Guidelines for Performing Systematic Literature Reviews in Software Engineering. Technical Report EBSE 2007-001, Keele University and Durham University Joint Report, 2007

    2007

  26. [26]

    Springer Berlin Heidelberg, Berlin, Heidelberg, Germany, 2004

    Edmund Clarke, Daniel Kroening, and Flavio Lerda.A Tool for Checking ANSI-C Programs, page 168–176. Springer Berlin Heidelberg, Berlin, Heidelberg, Germany, 2004. ISBN 9783540247302. doi: 10.1007/978-3-540-24730-2_15

    work page doi:10.1007/978-3-540-24730-2_15 2004

  27. [27]

    Erkan Keremoglu

    Dirk Beyer and M. Erkan Keremoglu. CPAchecker: A tool for configurable software verification. InProceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011), volume 6806 ofLecture Notes in Computer Science, pages 184–190, Snowbird, UT, USA, 2011. Springer. doi: 10.1007/978-3-642-22110-1_16

    work page doi:10.1007/978-3-642-22110-1_16 2011

  28. [28]

    Ultimate Automizer with array interpolation

    Matthias Heizmann, Daniel Dietsch, Vincent Langenfeld, and Andreas Podelski. Ultimate Automizer with array interpolation. InProceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), volume 7795 ofLecture Notes in Computer Science, pages 455–457, Rome, Italy, 2013. Springer

    2013

  29. [29]

    2LS for program analysis

    Martin Brain, Saurabh Joshi, Daniel Kroening, and Peter Schrammel. 2LS for program analysis. InProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), volume 9636 ofLecture Notes in Computer Science, pages 98–104, Eindhoven, The Netherlands,

    2016

  30. [30]

    doi: 10.1007/978-3-662-49674-9_6

    Springer. doi: 10.1007/978-3-662-49674-9_6

    work page doi:10.1007/978-3-662-49674-9_6

  31. [31]

    Symbiotic 7: Integration of a new slicer

    Marek Chalupa, Jan Strejˇcek, and Martin Višˇnovský. Symbiotic 7: Integration of a new slicer. InProceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), volume 12079 ofLecture Notes in Computer Science, pages 413–417, Dublin, Ireland, 2020. Springer. doi: 10.1007/978-3-030-45237-7...

    work page doi:10.1007/978-3-030-45237-7_27 2020

  32. [32]

    DiVinE 3.0 – an explicit-state LTL model checker

    Jiˇrí Barnat et al. DiVinE 3.0 – an explicit-state LTL model checker. InProceedings of the 25th International Conference on Computer Aided Verification (CAV 2013), volume 8044 ofLecture Notes in Computer Science, pages 863–868, Saint Petersburg, Russia, 2013. Springer. doi: 10.1007/978-3-642-39799-8_60

    work page doi:10.1007/978-3-642-39799-8_60 2013

  33. [33]

    Theta: A framework for abstraction refinement-based model checking

    Tamás Tóth, Ákos Hajdu, András Vörös, Zoltán Micskei, and István Majzik. Theta: A framework for abstraction refinement-based model checking. InProceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017), pages 176–179, Vienna, Austria, 2017. IEEE. doi: 10.23919/fmcad.2017.8102257

    work page doi:10.23919/fmcad.2017.8102257 2017

  34. [34]

    Verifying dynamic trait objects in Rust

    Alexa VanHattum, Daniel Schwartz-Narbonne, Nathan Chong, and Alberto Griggio. Verifying dynamic trait objects in Rust. InProceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice Track (ICSE-SEIP 2022), pages 321–330, Pittsburgh, PA, USA, 2022. ACM. doi: 10.1145/3510457.3513031

    work page doi:10.1145/3510457.3513031 2022

  35. [35]

    Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. The SeaHorn verification framework. InProceedings of the 27th International Conference on Computer Aided Verification (CAV 2015), volume 9206 ofLecture Notes in Computer Science, pages 343–361, San Francisco, CA, USA, 2015. Springer. doi: 10.1007/978-3-319-21690-4_20

    work page doi:10.1007/978-3-319-21690-4_20 2015

  36. [36]

    Z3: An Efficient SMT Solver

    Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. InProceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 200), volume 4963 ofLecture Notes in Computer Science, pages 337–340, Budapest, Hungary, 2008. Springer. doi: 10.1007/ 978-3-540-78800-3_24

    2008

  37. [37]

    Bitwuzla

    Aina Niemetz and Mathias Preiner. Bitwuzla. InComputer Aided Verification, page 3–17, Cham, Switzerland,

  38. [38]

    ISBN 9783031377037

    Springer Nature Switzerland. ISBN 9783031377037. doi: 10.1007/978-3-031-37703-7_1

    work page doi:10.1007/978-3-031-37703-7_1

  39. [39]

    Schaafsma, and Roberto Sebastiani

    Alessandro Cimatti, Alberto Griggio, Bastiaan J. Schaafsma, and Roberto Sebastiani. The MathSAT5 SMT Solver. InProceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), volume 7795 ofLecture Notes in Computer Science, pages 93–107, Rome, Italy, 2013. Springer. doi: 10.1007/978-3-642...

    work page doi:10.1007/978-3-642-36742-7_7 2013

  40. [40]

    cvc5: A Versatile and Industrial-Strength SMT Solver

    Haniel Barbosa et al. cvc5: A Versatile and Industrial-Strength SMT Solver. InProceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), volume 13243 ofLecture Notes in Computer Science, pages 415–442, Munich, Germany, 2022. Springer. doi: 10.1007/978-3-030-99524-9_24

    work page doi:10.1007/978-3-030-99524-9_24 2022

  41. [41]

    Yices 2.2

    Bruno Dutertre. Yices 2.2. InProceedings of the 26th International Conference on Computer-Aided Verification (CAV 2014), volume 8559 ofLecture Notes in Computer Science, pages 737–744, Vienna, Austria, 2014. Springer. doi: 10.1007/978-3-319-08867-9_49

    work page doi:10.1007/978-3-319-08867-9_49 2014

  42. [42]

    Clarke and E

    Edmund M. Clarke and E. Allen Emerson.Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic, page 52–71. Springer-Verlag, Berlin, Heidelberg, Germany, 1982. ISBN 354011212X. doi: 10.1007/bfb0025774

    work page doi:10.1007/bfb0025774 1982

  43. [43]

    Clarke.Model checking

    Edmund M. Clarke.Model checking. Springer Berlin Heidelberg, Berlin, Heidelberg, 1997. ISBN 9783540696599. doi: 10.1007/bfb0058022

    work page doi:10.1007/bfb0058022 1997

  44. [44]

    Bryant , title =

    Bryant. Graph-Based Algorithms for Boolean Function Manipulation.IEEE Transactions on Computers, C–35 (8):677–691, August 1986. ISSN 2326-3814. doi: 10.1109/tc.1986.1676819

    work page doi:10.1109/tc.1986.1676819 1986

  45. [45]

    Clarke, William Klieber, Miloš Nováˇcek, and Paolo Zuliani.Model Checking and the State Explosion Problem, page 1–30

    Edmund M. Clarke, William Klieber, Miloš Nováˇcek, and Paolo Zuliani.Model Checking and the State Explosion Problem, page 1–30. Springer Berlin Heidelberg, Berlin, Heidelberg, Germany, 2012. ISBN 9783642357466. doi: 10.1007/978-3-642-35746-6_1

    work page doi:10.1007/978-3-642-35746-6_1 2012

  46. [46]

    Checking Safety Properties Using Induction and a SAT-Solver

    Mary Sheeran, Satnam Singh, and Gunnar Stålmarck. Checking Safety Properties Using Induction and a SAT-Solver. InProceedings of the 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD 2000), volume 1954 ofLecture Notes in Computer Science, pages 108–125, Austin, TX, USA, 2000. Springer. doi: 10.1007/3-540-40922-X_8

    work page doi:10.1007/3-540-40922-x_8 2000

  47. [47]

    Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rümmer.Software Verification Using k-Induction, page 351–368

    Alastair F. Donaldson, Leopold Haller, Daniel Kroening, and Philipp Rümmer.Software Verification Using k-Induction, page 351–368. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. ISBN 9783642237027. doi: 10.1007/978-3-642-23702-7_26

    work page doi:10.1007/978-3-642-23702-7_26 2011

  48. [48]

    Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T).Journal of the ACM, 53(6):937–977, 2006

    Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T).Journal of the ACM, 53(6):937–977, 2006. doi: 10.1145/1217856.1217859

    work page doi:10.1145/1217856.1217859 2006

  49. [49]

    Springer Berlin Heidelberg, Berlin, Heidelberg, Germany, 2016

    Daniel Kroening and Ofer Strichman.Decision Procedures. Springer Berlin Heidelberg, Berlin, Heidelberg, Germany, 2016. ISBN 9783662504970. doi: 10.1007/978-3-662-50497-0. 38 ESBMC: A Survey of Its Evolution, Integration, and Future Directions in Formal Software Verification

    work page doi:10.1007/978-3-662-50497-0 2016

  50. [50]

    Springer Berlin Heidelberg, Berlin, Heidelberg, Germany, 2009

    Robert Brummayer and Armin Biere.Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays, page 174–177. Springer Berlin Heidelberg, Berlin, Heidelberg, Germany, 2009. ISBN 9783642007682. doi: 10.1007/978-3-642-00768-2_16

    work page doi:10.1007/978-3-642-00768-2_16 2009

  51. [51]

    Boolean Satisfiability Solvers and Their Applications in Model Checking.Proceedings of the IEEE, 103(11):2021–2035, November 2015

    Yakir Vizel, Georg Weissenbacher, and Sharad Malik. Boolean Satisfiability Solvers and Their Applications in Model Checking.Proceedings of the IEEE, 103(11):2021–2035, November 2015. ISSN 1558-2256. doi: 10.1109/jproc.2015.2455034

    work page doi:10.1109/jproc.2015.2455034 2021

  52. [52]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 2016

    Rajdeep Mukherjee, Michael Tautschnig, and Daniel Kroening.v2c – A Verilog to C Translator, page 580–586. Springer Berlin Heidelberg, Berlin, Heidelberg, 2016. ISBN 9783662496749. doi: 10.1007/978-3-662-49674-9_ 38

    work page doi:10.1007/978-3-662-49674-9_ 2016

  53. [53]

    SMT-Based Bounded Model Checking for Embedded ANSI-C Software

    Lucas Cordeiro, Bernd Fischer, and Joao Marques-Silva. SMT-Based Bounded Model Checking for Embedded ANSI-C Software. InProceedings of the 24th IEEE/ACM International Conference on Automated Software Engineering (ASE 2009), pages 137–148, Auckland, New Zealand, 2009. IEEE. doi: 10.1109/ASE.2009.17

    work page doi:10.1109/ase.2009.17 2009

  54. [54]

    Proceedings, volume 8413 ofLecture Notes in Computer Science, 2014

    Erika Ábrahám and Klaus Havelund, editors.Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13, 2014. Proceedings, volume 8413 ofLecture Notes in Computer Science, 2014. Spring...

    work page doi:10.1007/978-3-642-54862-8 2014

  55. [55]

    Gadelha, Rafael S

    Mikhail R. Gadelha, Rafael S. Menezes, and Lucas C. Cordeiro. ESBMC 6.1: Automated Test Case Generation Using Bounded Model Checking.International Journal on Software Tools for Technology Transfer, 23(6): 857–861, May 2020. ISSN 1433-2787. doi: 10.1007/s10009-020-00571-2

    work page doi:10.1007/s10009-020-00571-2 2020

  56. [56]

    ESBMC v7.7: Automating Branch Coverage Analysis Using CFG-Based Instrumentation and SMT Solving

    Rafael Menezes et al. ESBMC v7.7: Automating Branch Coverage Analysis Using CFG-Based Instrumentation and SMT Solving. InProceedings of the 28th International Conference on Fundamental Approaches to Software Engineering (FASE 2025), Lecture Notes in Computer Science, Hamilton, New Zealand, 2025. Springer. doi: 10.1007/978-3-031-90900-9_15

    work page doi:10.1007/978-3-031-90900-9_15 2025

  57. [57]

    Cordeiro, Bernd Fischer, and João Marques-Silva

    Lucas C. Cordeiro, Bernd Fischer, and João Marques-Silva. Verifying Multi-Threaded Software Using SMT- Based Context-Bounded Model Checking. InProceedings of the 33rd International Conference on Software Engineering (ICSE 2011), pages 331–340, Honolulu, HI, USA, 2011. ACM. doi: 10.1145/1985793.1985839

    work page doi:10.1145/1985793.1985839 2011

  58. [58]

    Verifying Embedded C Software with Timing Constraints Using an Untimed Bounded Model Checker

    Raimundo Barreto, Lucas Cordeiro, and Bernd Fischer. Verifying Embedded C Software with Timing Constraints Using an Untimed Bounded Model Checker. In2011 Brazilian Symposium on Computing System Engineering, page 46–52, Los Alamitos, CA, USA, November 2011. IEEE. doi: 10.1109/sbesc.2011.19

    work page doi:10.1109/sbesc.2011.19 2011

  59. [59]

    Mikhail Y . R. Gadelha, Lucas C. Cordeiro, and Denis A. Nicole. Encoding Floating-Point Numbers Using the SMT Theory in ESBMC: An Empirical Evaluation over the SV-COMP Benchmarks. InProceedings of the 22nd International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2017), volume 10471 ofLecture Notes in Computer Science, pages 91–106, ...

    2017

  60. [60]

    Gadelha, Konstantin Korovin, Giles Reger, and Lucas C

    Franz Brauße, Fedor Shmarov, Rafael Menezes, Mikhail R. Gadelha, Konstantin Korovin, Giles Reger, and Lucas C. Cordeiro. ESBMC-CHERI: Towards Verification of C Programs for CHERI Platforms with ESBMC. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2022), pages 773–776, Seoul, South Korea, July 2022. ...

    work page doi:10.1145/3533767.3543289 2022

  61. [61]

    Phd thesis, The University of Manchester, June 2025

    Rafael Sá Menezes.GOTO: a verification framework for CProver tools. Phd thesis, The University of Manchester, June 2025. URL https://ssvlab.github.io/lucasccordeiro/supervisions/phd_thesis_rafael. pdf

    2025

  62. [62]

    LLM For Loop Invariant Generation and Fixing: How Far Are We?, 2025

    Mostafijur Rahman Akhond, Saikat Chakraborty, and Gias Uddin. LLM For Loop Invariant Generation and Fixing: How Far Are We?, 2025

    2025

  63. [63]

    Ferreira, Pedro Cruz, Thomas Durieux, and Rui Abreu

    João F. Ferreira, Pedro Cruz, Thomas Durieux, and Rui Abreu. Smartbugs: A framework to analyze solidity smart contracts, 2020. URLhttps://arxiv.org/abs/2007.04771

    work page arXiv 2020

  64. [64]

    Whalen, Lee Pike, Adam Foltzer, Michal Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser, and Douglas Stuart

    Darren Cofer, Andrew Gacek, John Backes, Michael W. Whalen, Lee Pike, Adam Foltzer, Michal Podhradsky, Gerwin Klein, Ihor Kuz, June Andronick, Gernot Heiser, and Douglas Stuart. A Formal Approach to Constructing Secure Air Vehicle Software.Computer, 51(11):14–23, November 2018. ISSN 1558-0814. doi: 10.1109/mc. 2018.2876051

    work page doi:10.1109/mc 2018

  65. [65]

    Cordeiro, and Vasileios Mavroeidis

    Norbert Tihanyi, Tamas Bisztray, Ridhi Jain, Mohamed Amine Ferrag, Lucas C. Cordeiro, and Vasileios Mavroeidis. The FormAI Dataset: Generative AI in Software Security through the Lens of Formal Verification. InProceedings of the 19th International Conference on Predictive Models and Data Analytics in Software Engineering (PROMISE 2023), pages 33–40, San F...

    work page doi:10.1145/3617555 2023

  66. [66]

    Dubniczky, Ridhi Jain, and Lucas C

    Norbert Tihanyi, Tamas Bisztray, Mohamed Amine Ferrag, Bilel Cherif, Richard A. Dubniczky, Ridhi Jain, and Lucas C. Cordeiro. Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview, 2025

    2025

  67. [67]

    Attention is all you need

    Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Ł ukasz Kaiser, and Illia Polosukhin. Attention is all you need. In I. Guyon, U. V on Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, editors,Advances in Neural Information Processing Systems, volume 30, Long Beach, CA, USA, 2017. Curran Ass...

    2017

  68. [68]

    Language models are few-shot learners

    Tom Brown et al. Language models are few-shot learners. In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin, editors,Advances in Neural Information Processing Systems, volume 33, pages 1877– 1901, Vancouver, Canada, 2020. Curran Associates, Inc. URLhttps://proceedings.neurips.cc/paper_ files/paper/2020/file/1457c0d6bfcb4967418bfb8ac142f64a-Paper.pdf

    1901

  69. [69]

    Asleep at the Keyboard? Assessing the Security of GitHub Copilot’s Code Contributions.Communications of the ACM, 68(2): 96–105, January 2025

    Hammond Pearce, Baleegh Ahmad, Benjamin Tan, Brendan Dolan-Gavitt, and Ramesh Karri. Asleep at the Keyboard? Assessing the Security of GitHub Copilot’s Code Contributions.Communications of the ACM, 68(2): 96–105, January 2025. ISSN 1557-7317. doi: 10.1145/3610721

    work page doi:10.1145/3610721 2025

  70. [70]

    A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation, 2023

    Xiaowei Huang, Wenjie Ruan, Wei Huang, Gaojie Jin, Dong, et al. A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation, 2023

    2023

  71. [71]

    Springer Nature Switzerland, Cham, Switzerland, October 2024

    Bernhard Beckert, Jonas Klamroth, Wolfram Pfeifer, Patrick Röper, and Samuel Teuber.Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification, page 242–257. Springer Nature Switzerland, Cham, Switzerland, October 2024. ISBN 9783031753879. doi: 10.1007/978-3-031-75387-9_15

    work page doi:10.1007/978-3-031-75387-9_15 2024

  72. [72]

    Barrett, and Nina Narodytska

    Haoze Wu, Clark W. Barrett, and Nina Narodytska. Lemur: Integrating Large Language Models in Automated Program Verification. InThe Twelfth International Conference on Learning Representations (ICLR 2024), page 7652, Vienna, Austria, 2024. OpenReview.net. URLhttps://openreview.net/forum?id=Q3YaCghZNt

    2024

  73. [73]

    Cordeiro

    Lucas C. Cordeiro. Lucas Cordeiro — Systems and Software Verification Laboratory (SSVLab) Personal Page. https://ssvlab.github.io/lucasccordeiro/, 2025. Accessed: May 2026

    2025

  74. [74]

    R&D Investments Spearhead Push to Block Cyber Security Attacks (Soteria consortium, £5.8M)

    UK Research and Innovation (UKRI). R&D Investments Spearhead Push to Block Cyber Security Attacks (Soteria consortium, £5.8M). https://www.openaccessgovernment.org/ rd-investments-spearhead-cyber-security-defence/96958/, 2021

    2021

  75. [75]

    ELEGANT — Towards Attestable and Trustworthy Internet-of-Things Infrastructures (H2020 grant agreement No

    European Commission. ELEGANT — Towards Attestable and Trustworthy Internet-of-Things Infrastructures (H2020 grant agreement No. 957286). CORDIS — EU Research Results. https://cordis.europa.eu/ project/id/957286, 2021. Accessed: May 2026

    2021

  76. [76]

    Digital Security by Design (DSbD) Programme

    UK Research and Innovation (UKRI). Digital Security by Design (DSbD) Programme. https://www.ukri.org/what-we-do/browse-our-areas-of-investment-and-support/ digital-security-by-design/, 2019. Accessed: May 2026

    2019

  77. [77]

    VeriBee: Source Code Security (Research Impact Record)

    University of Manchester Research Explorer. VeriBee: Source Code Security (Research Impact Record). https://research.manchester.ac.uk/en/impacts/veribee-source-code-security/ , 2025. Ac- cessed: May 2026

    2025

  78. [78]

    UK SMEs Face Rise in Cyber Attacks with Average Cost £7,960.https://securitybrief

    SecurityBrief UK. UK SMEs Face Rise in Cyber Attacks with Average Cost £7,960.https://securitybrief. co.uk/story/uk-smes-face-rise-in-cyber-attacks-with-average-cost-gbp-7-960 , 2024. Ac- cessed: May 2026

    2024

  79. [79]

    The Economic Impacts of Inadequate Infrastructure for Software Testing

    Gregory Tassey. The Economic Impacts of Inadequate Infrastructure for Software Testing. Technical Report Planning Report 02-3, National Institute of Standards and Technology (NIST), Gaithersburg, MD, 2002. URL https://www.nist.gov/document/report02-3pdf. Accessed: May 2026

    2002

  80. [80]

    The cost of poor software quality in the US: A 2020 report

    Consortium for Information and Software Quality. The cost of poor software quality in the US: A 2020 report. Technical report, CISQ, 2020. URL https://www.it-cisq.org/ the-cost-of-poor-software-quality-in-the-us-a-2020-report/

    2020

Showing first 80 references.