Skip to content
DraconiticResearch
Search Sources API
203,234 studies31 sourcesUpdated 29 min ago
Peer-reviewedCC BY 4.0PLOS One

Automated loop invariant inference through learning-guided program structure analysis

  • Abeer S. Hadad1
  • Jiangbin Zheng1
  • Adeeb A. Ahmed2
  • Fahman Saeed3
  • Mohammad Alkhatib3
  • Safa Hussein Mohammed4
4 affiliations
  1. 1School of Software, Northwestern Polytechnical University, Xi’an, Shaanxi, China
  2. 2School of Electro-Mechanical Engineering, Xidian University, Xi’an, Shaanxi, China
  3. 3College of Computer and Information Sciences, Imam Mohammad Ibn Saud Islamic University (IMSIU), Riyadh, Saudi Arabia
  4. 4School of Electronics and Information, Northwestern Polytechnical University, Xi’an, Shaanxi, China
Read full textPDFDOICite

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.

Related

  1. Interpretable Processing–Structure Relationships in Spirulina Bioplastics through Automated Spectral and Microstructural Analysis
    Kuotian Liao, Yiyang Sun, Ian R. Campbell +10
    ChemRxivPreprintCC BYMaterials & polymersChemRxiv
  2. Pushing the Limits of One-Dimensional NMR Spectroscopy for Automated Structure Elucidation Using Artificial Intelligence
    Frank Hu, J. A. Tubb, Dimitris Argyropoulos +5
    Journal of Chemical Information and ModelingPeer-reviewedLicence not statedFull text11 citedMedicinal chemistry & drug discoveryPhysical chemistryOpenAlex
  3. Automated Static and Dynamic Contact-Angle Analysis with Machine Learning
    Daniel G.Shaw, Jianzhong Qi, Joseph D. Berry
    ChemRxivPreprintLicence not statedGeneral chemistryChemRxiv
  4. Chemistry-Informed Multimodal Model for Structure Elucidation in Automated Reaction Discovery
    Maik G. Niedziella, Philipp M. Pflüger, Ajnabiul Hoque +1
    ChemRxivPreprintCC BYFull textPhysical chemistryChemRxiv
  5. Context-Aware Automated NMR Structure Elucidation
    Frank Hu, Jonathan M. Tubb, Grant M. Rotskoff +2
    arXivPreprintCC BY 4.0Full textPhysical chemistryarXiv

Cite

BibTeXRIS
BibTeX
@article{hadad2026automated,
  title = {{Automated loop invariant inference through learning-guided program structure analysis}},
  author = {Abeer S. Hadad and Jiangbin Zheng and Adeeb A. Ahmed and Fahman Saeed and Mohammad Alkhatib and Safa Hussein Mohammed},
  journal = {PLOS One},
  year = {2026},
  month = oct,
  doi = {10.1371/journal.pone.0360726},
  url = {https://doi.org/10.1371/journal.pone.0360726},
  note = {CC BY 4.0},
}
RIS
TY  - JOUR
TI  - Automated loop invariant inference through learning-guided program structure analysis
AU  - Abeer S. Hadad
AU  - Jiangbin Zheng
AU  - Adeeb A. Ahmed
AU  - Fahman Saeed
AU  - Mohammad Alkhatib
AU  - Safa Hussein Mohammed
PY  - 2026
DA  - 2026/10/27
JO  - PLOS One
DO  - 10.1371/journal.pone.0360726
UR  - https://doi.org/10.1371/journal.pone.0360726
AB  - 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.
SN  - 1932-6203
ER  -