Inferring Loop Invariants for Multi-Path Loops

Loop invariant plays an important role in program analysis and verification. Equipping each loop with a sound and useful invariant is a crucial step for full program verification and program understanding. However, inferring sound and useful loop invariants remains a challenge due to the complex control structure of loops, especially for loops that contain multiple paths. In this paper, we first analyze the main challenges in loop invariant inference, then introduce a new approach to generate sound and useful loop invariants using a divide-and-conquer strategy. Specifically, we use Path Dependency Automaton (PDA) to model loops by which we boil down the problem of loop invariant inference to state invariant inference of the PDA. We propose an algorithm to infer state invariants of the PDA and construct loop invariants from state invariants. We implement our approach in a tool named InvInfer. We evaluate InvInfer on various benchmarks. The results show that our approach is remarkably more effective and efficient than several state-of-the-art approaches, especially on loops with multiple paths.