Facilitating Verification in Program Loops by Identification of Static Iteration Patterns

Generating invariants for loops is often a grueling obstacle in formal program verification. Researchers have employed methods from formal techniques based on abstract interpretation to test-driven dynamic analysis to tackle this problem. Even though powerful techniques for generating conjunctive invariants (invariants that employ only conjunction of terms) have been developed, disjunctive invariants have remained a sore thumb for formal techniques. In this paper, we propose a technique to transform certain category of loops, those that have a static iteration pattern, into loops that can be handled by conjunctive invariant generators. The key idea is to identify a static iteration pattern that distributes the disjunction in an invariant in a manner that can be captured by only conjunctive invariants. To broaden the scope of our algorithm, we also propose the idea of parametric verification, while attempting to verify specialized versions of the program where a subset of the input variables is instantiated with certain test-inputs. Note that parametric verification distinguishes it from program testing as testing requires all of its variables to be instantiated with test-inputs. We discuss our ideas on loops drawn from real programs to establish real-world applicability of our algorithms.