mlsanityData to 7 Oct 2026

A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification

arXiv 2305.14752 ↗First posted 24 May 2023cs.SE cs.AI cs.FLcited by 42

Not on the map. Why?

Abstract (arXiv)

This paper introduces an innovative approach that combines Large Language Models (LLMs) with Formal Verification strategies for automatic software vulnerability repair. Initially, we employ Bounded Model Checking (BMC) to identify vulnerabilities and extract counterexamples. These counterexamples are supported by mathematical proofs and the stack trace of the vulnerabilities. Using a specially designed prompt, we combine the original source code with the identified vulnerability, including its stack trace and counterexample that specifies the line number and error type. This combined information is then fed into an LLM, which is instructed to attempt to fix the code. The new code is subsequently verified again using BMC to ensure the fix succeeded. We present the ESBMC-AI framework as a proof of concept, leveraging the well-recognized and industry-adopted Efficient SMT-based Context-Bounded Model Checker (ESBMC) and a pre-trained transformer model to detect and fix errors in C programs, particularly in critical software components. We evaluated our approach on 50,000 C programs randomly selected from the FormAI dataset with their respective vulnerability classifications. Our results demonstrate ESBMC-AI's capability to automate the detection and repair of issues such as buffer overflow, arithmetic overflow, and pointer dereference failures with high accuracy. ESBMC-AI is a pioneering initiative, integrating LLMs with BMC techniques, offering potential integration into the continuous integration and deployment (CI/CD) process within the software development lifecycle.

Key facts. Cited by 42 papers in the map (data through 7 Oct 2026). Builds on 52 of its 132 references that are in the map. First posted on arXiv 24 May 2023.

Builds on

52 of 132 references.

References · 52

  1. 2017Attention Is All You Needcited by 59,932
  2. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,204
  3. 2020Language Models are Few-Shot Learnerscited by 32,199
  4. 2019Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformercited by 14,491
  5. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  6. 2014Sequence to Sequence Learning with Neural Networkscited by 2,974
  7. 2023Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generationcited by 1,332
  8. 2021Measuring Coding Challenge Competence With APPScited by 879
  9. 2021CodeXGLUE: A Machine Learning Benchmark Dataset for Code Understanding and Generationcited by 732
  10. 2019CodeSearchNet Challenge: Evaluating the State of Semantic Code Searchcited by 638
  11. 2023A Prompt Pattern Catalog to Enhance Prompt Engineering with ChatGPTcited by 612
  12. 2021Prompt Programming for Large Language Models: Beyond the Few-Shot Paradigmcited by 599
38 more
  1. 2019Devign: Effective Vulnerability Identification by Learning Comprehensive Program Semantics via Graph Neural Networkscited by 266
  2. 2022Can language models learn from explanations in context?cited by 248
  3. 2023MathPrompter: Mathematical Reasoning using Large Language Modelscited by 236
  4. 2023OpenAGI: When LLM Meets Domain Expertscited by 196
  5. 2022GitHub Copilot AI pair programmer: Asset or Liability?cited by 150
  6. 2018SequenceR: Sequence-to-Sequence Learning for End-to-End Program Repaircited by 144
  7. 2020Deep Learning based Vulnerability Detection: Are We There Yet?cited by 142
  8. 2022Practical Program Repair in the Era of Large Pre-trained Language Modelscited by 133
  9. 2023Keep the Conversation Going: Fixing 162 out of 337 bugs for 0.42 each using ChatGPTcited by 125
  10. 2023InferFix: End-to-End Program Repair with LLMscited by 113
  11. 2023Self-Edit: Fault-Aware Code Editor for Code Generationcited by 110
  12. 2023An Analysis of the Automatic Bug Fixing Performance of ChatGPTcited by 108
  13. 2021Examining Zero-Shot Vulnerability Repair with Large Language Modelscited by 105
  14. 2021Jigsaw: Large Language Models meet Program Synthesiscited by 103
  15. 2022Large Language Models are Zero-Shot Fuzzers: Fuzzing Deep-Learning Libraries via Large Language Modelscited by 102
  16. 2021CURE: Code-Aware Neural Machine Translation for Automatic Program Repaircited by 85
  17. 2022Less Training, More Repairing Please: Revisiting Automated Program Repair via Zero-shot Learningcited by 76
  18. 2023Is ChatGPT the Ultimate Programming Assistant -- How far is it?cited by 72
  19. 2021Break-It-Fix-It: Unsupervised Learning for Program Repaircited by 71
  20. 2022Automated Repair of Programs from Large Language Modelscited by 71
  21. 2022Repair Is Nearly Generation: Multilingual Program Repair with LLMscited by 68
  22. 2021A Syntax-Guided Edit Decoder for Neural Program Repaircited by 57
  23. 2022NatGen: Generative pre-training by "Naturalizing" source codecited by 53
  24. 2022Compilable Neural Code Generation with Compiler Feedbackcited by 46
  25. 2023Conversational Automated Program Repaircited by 41
  26. 2019Getafix: Learning to Fix Bugs Automaticallycited by 40
  27. 2021Neural Transfer Learning for Repairing Security Vulnerabilities in C Codecited by 36
  28. 2023Large Language Models are Edge-Case Fuzzers: Testing Deep Learning Libraries via FuzzGPTcited by 36
  29. 2017Sorting and Transforming Program Repair Ingredients via Deep Learning Code Similaritiescited by 26
  30. 2023A study on Prompt Design, Advantages and Limitations of ChatGPT for Deep Learning Program Repaircited by 26
  31. 2021Automatic Program Repair with OpenAI's Codex: Evaluating QuixBugscited by 24
  32. 2022DEAR: A Novel Deep Learning-based Approach for Automated Program Repaircited by 22
  33. 2022Neurosymbolic Repair for Low-Code Formula Languagescited by 12
  34. 2023Reliable Natural Language Understanding with Large Language Models and Answer Set Programmingcited by 12
  35. 2023On pitfalls (and advantages) of sophisticated large language modelscited by 7
  36. 2018SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzercited by 5
  37. 2020MUZZ: Thread-aware Grey-box Fuzzing for Effective Bug Hunting in Multithreaded Programscited by 3
  38. 2021Model Checking C++ Programscited by 3

50 most cited of 52 All 52 (JSON)

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 10; 2024: 13; 2025: 13; 2026: 6.

42 papers.

Sort:

By area:

  1. 2023Large Language Models for Software Engineering: A Systematic Literature Reviewcited by 389
  2. 2023Automatically Correcting Large Language Models: Surveying the landscape of diverse self-correction strategiescited by 236
  3. 2024When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMscited by 230
  4. 2024Recursive Introspection: Teaching Language Model Agents How to Self-Improvecited by 162
  5. 2024Large Language Models for Cyber Security: A Systematic Literature Reviewcited by 65
  6. 2023Clover: Closed-Loop Verifiable Code Generationcited by 62
  7. 2024CyberMetric: A Benchmark Dataset based on Retrieval-Augmented Generation for Evaluating LLMs in Cybersecurity Knowledgecited by 55
  8. 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
  9. 2024Large Language Models in Cybersecurity: State-of-the-Artcited by 34
  10. 2023The FormAI Dataset: Generative AI in Software Security Through the Lens of Formal Verificationcited by 32
  11. 2024LLMs in Web Development: Evaluating LLM-Generated PHP Code Unveiling Vulnerabilities and Limitationscited by 21
  12. 2024PromSec: Prompt Optimization for Secure Generation of Functional Source Code with Large Language Models (LLMs)cited by 17
30 more
  1. 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofscited by 17
  2. 2025CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detectioncited by 10
  3. 2025Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overviewcited by 7
  4. 2023ZeroLeak: Using LLMs for Scalable and Cost Effective Side-Channel Patchingcited by 6
  5. 2024Helping LLMs Improve Code Generation Using Feedback from Testing and Static Analysiscited by 6
  6. 2026Self-Refining Vision Language Model for Robotic Failure Detection and Reasoningcited by 6
  7. 2024Think Thrice Before You Act: Progressive Thought Refinement in Large Language Modelscited by 5
  8. 2023LUNA: A Model-Based Universal Analysis Framework for Large Language Modelscited by 4
  9. 2024Enhancing Source Code Security with LLMs: Demystifying The Challenges and Generating Reliable Repairscited by 4
  10. 2024Automated Repair of AI Code with Large Language Models and Formal Verificationcited by 3
  11. 2024Towards Large Language Model Aided Program Refinementcited by 2
  12. 2025Do AI models help produce verified bug fixes?cited by 2
  13. 2023Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approachcited by 1
  14. 2025Using ML filters to help automated vulnerability repairs: when it helps and when it doesn'tcited by 1
  15. 2025A Blueprint for AI-Driven Software Quality: Integrating LLMs with Established Standardscited by 1
  16. 2025Leveraging Large Language Models for Command Injection Vulnerability Analysis in Python: An Empirical Study on Popular Open-Source Projectscited by 1
  17. 2025Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Modelscited by 1
  18. 2025Towards Automated Formal Verification of Backend Systems with LLMscited by 1
  19. 2025The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guaranteecited by 1
  20. 2026Cracking IoT Security: Can LLMs Outsmart Static Analysis Tools?cited by 1
  21. 2026ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verificationcited by 1
  22. 2023Leveraging Large Language Models for DRL-Based Anti-Jamming Strategies in Zero Touch Networkscited by 0
  23. 2023KEN: Kernel Extensions using Natural Languagecited by 0
  24. 2024TIPS: Threat Actor Informed Prioritization of Applications using SecEncodercited by 0
  25. 2025Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMscited by 0
  26. 2025Working Document -- Formalising Software Requirements with Large Language Modelscited by 0
  27. 2025LLMs as verification oracles for Soliditycited by 0
  28. 2026LLMs + Security = Troublecited by 0
  29. 2026More Yap Less Meaning: Uncovering Self-Improvement Behavior in SLMscited by 0
  30. 2026Bulkhead: Automated Semantic Detection and Remediation of Container Escape Vulnerabilitiescited by 0