# Towards General Loop Invariant Generation: A Benchmark of Programs with Memory Manipulation

arXiv: https://arxiv.org/abs/2311.10483 · HTML: https://mlsanity.com/paper/2311.10483/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Nov 2023.

## Built on by (most cited first, 7 of 7)

- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)
- [HoarePrompt: Structural Reasoning About Program Correctness in Natural Language](https://mlsanity.com/paper/2503.19599/) (2025)
- [Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis](https://mlsanity.com/paper/2509.21629/) (2025)
- [INPROVF: Leveraging Large Language Models to Repair High-level Robot Controllers from Assumption Violations](https://mlsanity.com/paper/2503.13660/) (2025)
- [Agentic Separation Logic Specification Synthesis](https://mlsanity.com/paper/2605.27531/) (2026)
- [Privilege and confidentiality in generative AI workflows](https://mlsanity.com/paper/2607.05479/) (2026)
- [SkillForge: Compositional Skill Synthesis with Verification-in-the-Loop for Generating Formally Verified Dafny Programs](https://mlsanity.com/paper/2608.29841/) (2026)

## Abstract (arXiv)

Program verification is vital for ensuring software reliability, especially in the context of increasingly complex systems. Loop invariants, remaining true before and after each iteration of loops, are crucial for this verification process. Traditional provers and machine learning based methods for generating loop invariants often require expert intervention or extensive labeled data, and typically only handle numerical property verification. These methods struggle with programs involving complex data structures and memory manipulations, limiting their applicability and automation capabilities. In this paper, we introduce a new benchmark named LIG-MM, specifically for programs with complex data structures and memory manipulations. We collect 312 programs from various sources, including daily programs from college homework, the international competition (SV-COMP), benchmarks from previous papers (SLING), and programs from real-world software systems (Linux Kernel, GlibC, LiteOS, and Zephyr). Based on LIG-MM, our findings indicate that previous methods, including GPT-4, fail to automate verification for these programs. Consequently, we propose a novel LLM-SE framework that coordinates LLM with symbolic execution, fine-tuned using self-supervised learning, to generate loop invariants. Experimental results on LIG-MM demonstrate that our LLM-SE outperforms state-of-the-art methods, offering a new direction toward automated program verification in real-world scenarios.