Loops and other unbound control structures constitute a major bottleneck
in formal software verification, because correctness proofs over such
control structures generally require user interaction: typically, induction
hypotheses or invariants must be found or modified by hand. Such interaction
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. A loop can be parallelized, whenever the execution of a generic
iteration of its body depends only on the step parameter and not on other
iterations.
We use a symbolic dependence analysis that ensures parallelizability. This
guarantees soundness of a proof rule that transforms a loop into a universally
quantified update of the state change information effected by the loop body.
This rule makes it possible to employ automatic first-order reasoning
techniques to deal with loops.
The method has been implemented in the KeY verification tool. We evaluated its
applicability with representative case studies from the JavaCard domain.