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 a...