BALI: Branch-Aware Loop Invariant Inference with Large Language Models

TL;DR

BALI is a novel framework that leverages large language models and branch-aware static analysis to automate and improve the inference of loop invariants in complex programs, enhancing correctness verification.

Contribution

BALI introduces a branch-aware approach combining LLMs with SMT-based verification for scalable, automated loop invariant inference, surpassing prior guess-and-check methods.

Findings

Improved invariant inference accuracy.

Enhanced scalability for complex programs.

Effective integration of LLMs with static analysis.

Abstract

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.