Loops are a major bottleneck in formal software verification, because they
generally require user interaction: typically, induction hypotheses or
invariants must be found or modified by hand. This involves expert knowledge
of the underlying calculus and proof engine.
We show that one can replace interactive proof techniques, such as induction,
with automated first-order reasoning in order to deal with parallelizable
loops, where a loop can be parallelized whenever it avoids dependence of the
loop iterations from each other.
We develop a dependence analysis that ensures parallelizability. It guarantees
soundness of a proof rule that transforms a loop into a universally quantified
update of the state change information represented by the loop body. This
makes it possible to use automatic first order reasoning techniques to deal with
loops.
The method has been implemented in the KeY verification tool. We evaluated it
with representative case studies from the JavaCard domain.