Automated loop invariant inference through learning-guided program structure analysis.

Authors

Abeer S Hadad, Jiangbin Zheng, Adeeb A Ahmed, Fahman Saeed, Mohammad Alkhatib, Safa Hussein Mohammed

Published in

PloS one. Volume 21. Issue 10. Pages e0360726. Epub Oct 27, 2026.

Abstract

Automated loop invariant inference remains a fundamental challenge in formal verification due to the inherently unbounded search space of candidate invariants. Existing approaches either incur substantial computational overhead during invariant synthesis or rely on manually predefined templates, limiting both scalability and automation. Although recent learning-based methods have shown promise, they often fail to fully exploit the rich structural and semantic information embedded within program representations. This paper presents a learning-guided framework for fully automated loop invariant inference based on a systematic analysis of program structure and semantics. The framework performs a joint analysis of syntactic constructs, control-flow structure, and data-dependence relationships to determine invariant structure before instantiation. These complementary representations are embedded and integrated within a learning-based model that identifies structurally and semantically features and infers expressive invariant templates directly from program structure. The inferred templates are instantiated using execution-derived values, yielding constraint systems that are solved and formally validated using a Satisfiability Modulo Theories solver. Experimental evaluation demonstrates that the proposed approach achieves competitive invariant inference performance on challenging benchmarks. By integrating multi-representation program analysis, the framework effectively supports a wide range of loop structures and advances the state of the art in scalable, expressive, and fully automated loop invariant inference.

PMID:
42945349
Bibliographic data and abstract were imported from PubMed on 28 Oct 2026.

Read full publication at:
Please sign in to see all details.

Stats

1-terrible, 9-excellent. How would you rate this publication? Sign in in to submit your rating.

Post a comment

You need to be signed in to post comments. You can sign in here.

Comments

There are no comments yet.