{
  "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.",
  "abstract_shown": true,
  "affiliations": [
    "School of Software, Northwestern Polytechnical University, Xi’an, Shaanxi, China",
    "School of Electro-Mechanical Engineering, Xidian University, Xi’an, Shaanxi, China",
    "College of Computer and Information Sciences, Imam Mohammad Ibn Saud Islamic University (IMSIU), Riyadh, Saudi Arabia",
    "School of Electronics and Information, Northwestern Polytechnical University, Xi’an, Shaanxi, China"
  ],
  "article_type": "Research Article",
  "arxiv": null,
  "author_total": 6,
  "authors": [
    {
      "affs": [
        0
      ],
      "name": "Abeer S. Hadad",
      "orcid": "0000-0003-4332-7487"
    },
    {
      "affs": [
        0
      ],
      "name": "Jiangbin Zheng"
    },
    {
      "affs": [
        1
      ],
      "name": "Adeeb A. Ahmed"
    },
    {
      "affs": [
        2
      ],
      "name": "Fahman Saeed"
    },
    {
      "affs": [
        2
      ],
      "name": "Mohammad Alkhatib"
    },
    {
      "affs": [
        3
      ],
      "name": "Safa Hussein Mohammed"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/97s6w01ygmqsq.bib",
  "cited_by": 0,
  "doi": "10.1371/journal.pone.0360726",
  "fulltext_url": "https://pmc.ncbi.nlm.nih.gov/articles/PMC13712695/",
  "id": "97s6w01ygmqsq",
  "issns": [
    "1932-6203"
  ],
  "landing_url": "https://doi.org/10.1371/journal.pone.0360726",
  "language": "en",
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "https://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": null,
  "native_subjects": [
    [
      "heading",
      "Algebra"
    ],
    [
      "heading",
      "Artificial Intelligence"
    ],
    [
      "heading",
      "Built Structures"
    ],
    [
      "heading",
      "Composite Materials"
    ],
    [
      "heading",
      "Computer Software"
    ],
    [
      "heading",
      "Computer and Information Sciences"
    ],
    [
      "heading",
      "Concrete"
    ],
    [
      "heading",
      "Engineering and Technology"
    ],
    [
      "heading",
      "Grammar"
    ],
    [
      "heading",
      "Linguistics"
    ],
    [
      "heading",
      "Machine Learning"
    ],
    [
      "heading",
      "Materials"
    ],
    [
      "heading",
      "Materials Science"
    ],
    [
      "heading",
      "Mathematics"
    ],
    [
      "heading",
      "Physical Sciences"
    ],
    [
      "heading",
      "Polynomials"
    ],
    [
      "heading",
      "Research Article"
    ],
    [
      "heading",
      "Semantics"
    ],
    [
      "heading",
      "Social Sciences"
    ],
    [
      "heading",
      "Software Engineering"
    ],
    [
      "heading",
      "Source Code"
    ],
    [
      "heading",
      "Structural Engineering"
    ],
    [
      "heading",
      "Syntax"
    ],
    [
      "openalex",
      "1702|Logic, programming, and type systems"
    ],
    [
      "plos",
      "/Computer and information sciences/Artificial intelligence/Machine learning"
    ],
    [
      "plos",
      "/Computer and information sciences/Software engineering/Computer software"
    ],
    [
      "plos",
      "/Computer and information sciences/Software engineering/Source code"
    ],
    [
      "plos",
      "/Engineering and technology/Software engineering/Computer software"
    ],
    [
      "plos",
      "/Engineering and technology/Software engineering/Source code"
    ],
    [
      "plos",
      "/Engineering and technology/Structural engineering/Built structures"
    ],
    [
      "plos",
      "/Physical sciences/Materials science/Materials/Composite materials/Concrete"
    ],
    [
      "plos",
      "/Physical sciences/Mathematics/Algebra/Polynomials"
    ],
    [
      "plos",
      "/Social sciences/Linguistics/Grammar/Syntax"
    ],
    [
      "plos",
      "/Social sciences/Linguistics/Semantics"
    ]
  ],
  "openalex": "W7224006922",
  "pdf_url": "https://journals.plos.org/plosone/article/file?id=10.1371/journal.pone.0360726&type=printable",
  "pmcid": "PMC13712695",
  "pmid": "42945349",
  "published": "2026-10-27",
  "publisher": "Public Library of Science",
  "ris": "https://research.draconitic.com/paper/97s6w01ygmqsq.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:17:17Z",
      "native_id": "10.1371/journal.pone.0360726",
      "source": "plos",
      "url": "https://doi.org/10.1371/journal.pone.0360726"
    },
    {
      "first_seen": "2026-10-31T12:23:13Z",
      "native_id": "PMC13712695",
      "source": "pmc",
      "url": "https://doi.org/10.1371/journal.pone.0360726"
    }
  ],
  "subjects": [
    {
      "field": "chemistry",
      "origin": "plos:materials science",
      "subfield": "materials-polymers"
    },
    {
      "field": "mathematics",
      "origin": "plos:algebra",
      "subfield": "algebra-number-theory"
    }
  ],
  "title": "Automated loop invariant inference through learning-guided program structure analysis",
  "title_text": "Automated loop invariant inference through learning-guided program structure analysis",
  "type": "peer-reviewed",
  "updated_at": "2026-10-31T12:23:13Z",
  "url": "https://research.draconitic.com/paper/97s6w01ygmqsq",
  "venue": "PLOS One",
  "versions": []
}