CoChat
Sign Up
PreprintCited by 7Logic, programming, and type systemsSoftware Testing and Debugging TechniquesFormal Methods in Verification

The DOI matches its DataCite record; 20 of the 20 references it cites were found in a registry or an index.

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

Open access
Liu, Chang, Wu, Xiwei, Feng, Yuan, Cao, Qinxiang, Yan, Junchi·2023·arXiv
DOI 10.48550/arxiv.2311.10483arXiv 2311.10483
Open this paper in CoChat — free accountOpen PDF

Abstract

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.

Overview

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.2311.10483

Cites

20 of 20 references verified0 citation errors · 0 not checkable

Statistics

Verification

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Many existing works combine LLMs and formal methods, highlighting the ability of LLMs to effectively incorporate feedback from a verification engine.

    “Many existing works combine LLMs and formal methods, highlighting the ability of LLMs to effectively incorporate feedback from a verification engine.”

    From Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification (2025) · cites this paper as [20]

    Section 4.2 describes this paper’s interactive framework, in which verification tools check and refine LLM-generated terms, and the updated assertions are used in subsequent inference. The paper thus supports an example of LLM–formal-methods collaboration, but it does not establish that many existing works demonstrate LLMs effectively incorporating verification-engine feedback. (LLM, conf=0.85)

    Experimental — accuracy not yet measured

  • Type I systems use formal methods to filter out solutions that do not satisfy a specification and provide feedback to the LLM, iterating until a valid solution is reached.

    “Type I systems (Figure 2, left) use formal methods to filter out solutions that do not satisfy a certain specification, and provide feedback (e.g., a counterexample) to the LLM, iterating until a valid solution is reached (e.g., loop-invariant synthesis with formal tools in the loop [2, 12, 20, 21, 38], static analysisguided repair [27]).”

    From Position: Vibe Coding Needs Vibe Reasoning: Improving Vibe Coding with Formal Verification (2025) · cites this paper as [20]

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Citations

Cites

Flagged first, then by citations

Research works printed but not linked: 26

  1. K. Sieber, The foundations of program verification. Springer-Verlag, 2013.
  2. J. H. Fetzer, "Program verification: The very idea," Communications of the ACM, vol. 31, no. 9, pp. 1048-1063, 1988.
  3. S. Srivastava, S. Gulwani, and J. S. Foster, "From program verification to program synthe- sis," in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2010, pp. 313-326.
  4. J. B. Almeida, M. J. Frade, J. S. Pinto, and S. M. De Sousa, Rigorous software development: an introduction to program verification. Springer, 2011, vol. 1.
  5. P. Koopman and M. Wagner, "Challenges in autonomous vehicle testing and validation," SAE International Journal of Transportation Safety, vol. 4, no. 1, pp. 15-24, 2016.
  6. Z. Daw, R. Cleaveland, and M. Vetter, "Formal verification of software-based medical devices considering medical guidelines," International journal of computer assisted radiology and surgery, vol. 9, pp. 145-153, 2014.
  7. C. Colombo and G. J. Pace, "Industrial experiences with runtime verification of financial transaction systems: lessons learnt and standing challenges," in Lectures on Runtime Verification: Introductory and Advanced Topics. Springer, 2018, pp. 211-232.
  8. T. Dreossi, D. J. Fremont, S. Ghosh, E. Kim, H. Ravanbakhsh, M. Vazquez-Chanlatte, and S. A. Seshia, "Verifai: A toolkit for the formal design and analysis of artificial intelligence-based systems," in International Conference on Computer Aided Verification. Springer, 2019, pp. 432-442.
  9. F. Rajaona, I. Boureanu, V. Malvone, and F. Belardinelli, "Program semantics and verification technique for ai-centred programs," in International Symposium on Formal Methods. Springer, 2023, pp. 473-491.
  10. C. A. R. Hoare, "An axiomatic basis for computer programming," Communications of the ACM, vol. 12, no. 10, pp. 576-580, 1969.
  11. C. A. Furia, B. Meyer, and S. Velder, "Loop invariants: Analysis, classification, and examples," ACM Computing Surveys (CSUR), vol. 46, no. 3, pp. 1-51, 2014.
  12. X. Si, H. Dai, M. Raghothaman, M. Naik, and L. Song, "Learning loop invariants for program verification," in Proceedings of the 32nd International Conference on Neural Information Processing Systems, ser. NIPS'18. Red Hook, NY, USA: Curran Associates Inc., 2018, p. 7762-7773.
  13. S. Padhi and T. D. Millstein, "Data-driven loop invariant inference with automatic feature synthesis," CoRR, vol. abs/1707.02029, 2017. [Online]. Available: http: //arxiv.org/abs/1707.02029 · arXiv
  14. S.-W. Lin, J. Sun, H. Xiao, Y. Liu, D. Sanán, and H. Hansen, "Fib: Squeezing loop invariants by interpolation between forward/backward predicate transformers," in 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2017, pp. 793- 803.
  15. J. Laurent and A. Platzer, "Learning to find proofs and theorems by learning to refine search strategies," CoRR, vol. abs/2205.14229, 2022. [Online]. Available: https://doi.org/10.48550/arXiv.2205.14229 · DOI
  16. R. Baldoni, E. Coppa, D. C. D'Elia, C. Demetrescu, and I. Finocchi, "A survey of symbolic execution techniques," ACM Comput. Surv., vol. 51, no. 3, 2018.
  17. E. Nijkamp, B. Pang, H. Hayashi, L. Tu, H. Wang, Y. Zhou, S. Savarese, and C. Xiong, "Codegen: An open large language model for code with multi-turn program synthesis," arXiv preprint arXiv:2203.13474, 2022. · arXiv
  18. S. Padhi, R. Sharma, and T. Millstein, "Data-driven precondition inference with learned features," ACM SIGPLAN Notices, vol. 51, no. 6, pp. 42-56, 2016.
  19. J.-C. Filliâtre and A. Paskevich, "Why3-where programs meet provers," in Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 22. Springer, 2013, pp. 125-128.
  20. M. Echenim, N. Peltier, and Y. Sellami, "A generic framework for implicate generation modulo theories," in Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings 9. Springer, 2018, pp. 279-294.
  21. L. De Moura and N. Bjørner, "Z3: An efficient smt solver," in International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 337-340.
  22. J. Laurent and A. Platzer, "Learning to find proofs and theorems by learning to refine search strategies: The case of loop invariant synthesis," Advances in Neural Information Processing Systems, vol. 35, pp. 4843-4856, 2022.
  23. J. Yao, G. Ryan, J. Wong, S. Jana, and R. Gu, "Learning nonlinear loop invariants with gated continuous logic networks," in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, 2020, pp. 106-120.
  24. M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao, "The daikon system for dynamic detection of likely invariants," Science of computer program- ming, vol. 69, no. 1-3, pp. 35-45, 2007.
  25. M. Bayer, M.-A. Kaufhold, and C. Reuter, "A survey on data augmentation for text classification," ACM Computing Surveys, vol. 55, no. 7, pp. 1-39, 2022.
  26. S. Yun, D. Han, S. J. Oh, S. Chun, J. Choe, and Y. Yoo, "Cutmix: Regularization strategy to train strong classifiers with localizable features," in Proceedings of the IEEE/CVF international conference on computer vision, 2019, pp. 6023-6032.

Cited by

Sorted by citations

Related

Metadata

Authors
Liu, C., Wu, X., Feng, Y., Cao, Q., & Yan, J.
ORCID
Venue
arXiv
Publisher
arXiv
Published
2023
Pages
129120-129145
ISSN
1049-5258 (ISSN-L)
DOI
10.48550/arxiv.2311.10483
arXiv
2311.10483
OpenAlex
W4415795200
Cited by
7
References
20
Citations by year
2026: 6 · 2025: 1
FWCI
2.02
Type
conference paper
Language
en
Open access
Licence
arxiv.org/licenses/nonexclusive-distrib/1.0/
Locations
  • neural information processing systems (publishedVersion)
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Topics
  • Physical Sciences › Computer Science › Software › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
Keywords
loop invariant generation, program verification, memory manipulation, benchmark programs, program analysis

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review