Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | https://arxiv.org/abs/2601.00882 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866908744716124160 |
|---|---|
| author | Wang, Mingxiu Wang, Jiawei Cheng, Xiao |
| author_facet | Wang, Mingxiu Wang, Jiawei Cheng, Xiao |
| contents | Loop invariants are fundamental for reasoning about the correctness of iterative algorithms. However, deriving suitable invariants remains a challenging and often manual task, particularly for complex programs. In this paper, we introduce BALI, a branch-aware framework that integrates large language models (LLMs) to enhance the inference and verification of loop invariants. Our approach combines automated reasoning with branch-aware static program analysis to improve both precision and scalability. Specifically, unlike prior LLM-only guess-and-check methods, BALI first verifies branch-sequence-level (path-level) clauses with SMT and then composes them into program-level invariants. We outline its key components, present preliminary results, and discuss future directions toward fully automated invariant discovery. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_00882 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | BALI: Branch-Aware Loop Invariant Inference with Large Language Models Wang, Mingxiu Wang, Jiawei Cheng, Xiao Programming Languages Loop invariants are fundamental for reasoning about the correctness of iterative algorithms. However, deriving suitable invariants remains a challenging and often manual task, particularly for complex programs. In this paper, we introduce BALI, a branch-aware framework that integrates large language models (LLMs) to enhance the inference and verification of loop invariants. Our approach combines automated reasoning with branch-aware static program analysis to improve both precision and scalability. Specifically, unlike prior LLM-only guess-and-check methods, BALI first verifies branch-sequence-level (path-level) clauses with SMT and then composes them into program-level invariants. We outline its key components, present preliminary results, and discuss future directions toward fully automated invariant discovery. |
| title | BALI: Branch-Aware Loop Invariant Inference with Large Language Models |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2601.00882 |