AutoINF: Path-Sensitive Invariant Inference for Multipath Loops

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.