AutoINF: Path-Sensitive Invariant Inference for Multipath Loops
Abeer S. Hadad1, Fahman Saeed2, Adeeb A. Ahmed3,*, Jiangbin Zheng1
1
School of Software, Northwestern Polytechnical University, Xi’an, China
2
College of Computer and Information Sciences, Imam Mohammad Ibn Saud Islamic University (IMSIU), Riyadh, Saudi Arabia
3
School of Electro-Mechanical Engineering, Xidian University, Xi’an, China
* Corresponding Author: Adeeb A. Ahmed. Email: adeebalgoidi@gmail.com
Computer Modeling in Engineering & Sciences https://doi.org/10.32604/cmes.2026.083873
Received 12 April 2026; Accepted 05 June 2026; Published online 29 June 2026
Abstract
Loop invariant inference is fundamental to program verification, yet it remains particularly challenging for multipath loops, where different execution paths may exhibit incompatible behaviors across feasible executions. In such settings, invariants that are both sound and sufficiently precise often require disjunctive forms, whose automatic inference remains difficult. This paper presents an efficient, path-sensitive, counterexample-guided framework for automated loop invariant inference. Our approach leverages a Path Dependency Automaton (PDA) to systematically decompose the semantics of multipath loops by modeling feasible execution paths independently. Building on this decomposition, we introduce a localized, path-guided Counterexample-Guided Invariant Refinement (CEGIR) process that validates candidate invariants against individual path semantics and uses targeted counterexamples to refine disjunctive and nonlinear polynomial invariant templates only where violations occur. We implement the proposed framework in AutoINF, an automated invariant inference tool for C programs containing multipath loops. The experimental evaluation on a diverse benchmark suite, including programs with complex control flow and nonlinear arithmetic, demonstrates that AutoINF infers sound and expressive invariants for challenging multipath loops.
Keywords
Numerical loop invariant; multipath loops; counterexample-guided refinement; program analysis and verification; software reliability; disjunctive invariants
Open Access
Login
Register
Submit a Paper
Propose a Special lssue
Download PDF
Downloads
Citation Tools
