Loop fusion—a program transformation to merge multiple consecutive loops into a single one—has been studied mainly for compiler optimization. In this paper, we argue that loop fusion can be useful also for program verification because it can simplify loop invariants and we propose a new loop fusion strategy, which can fuse any loops—even loops with data dependence—and preserves partial correctness.

The crux of our loop fusion is the following observation: if the state after the first loop were known, two loop bodies could be computed at the same time without suffering from data dependence by renaming program variables. Our loop fusion produces a program that guesses the unknown state after the first loop nondeterministically, executes the fused loop where variables are renamed, compares the guessed state and the state actually computed by the fused loop, and, if they do not match, diverges. The last two steps of comparison and divergence are crucial to preserve partial correctness. We call our approach ``guess-and-assume'' because, in addition to the first step to guess, the last two steps can be expressed by the pseudo-instruction assume, used in program verification.

We formalize our loop fusion for a simple imperative language and prove that it preserves partial correctness. We further extend the ``guess-and-assume'' technique to reversing loop execution, which is useful to verify a certain type of consecutive loops. Finally, we confirm by experiments that our transformation techniques can significantly reduce verification time in many cases.