We present combined-case k-induction, a novel technique for
verifying software programs. This technique draws on the strengths of the
classical inductive-invariant method and a recent application of
k-induction to program verification. In previous work, correctness of
programs was established by separately proving a base case and inductive
step. We present a new k-induction rule that takes an unstructured,
reducible control flow graph (CFG), a natural loop occurring in the CFG,
and a positive integer k, and constructs a single CFG in which
the given loop is eliminated via an unwinding proportional to k.
Recursively applying the proof rule eventually yields a loop-free CFG,
which can be checked using SAT-/SMT-based techniques.
We state soundness of the rule, and investigate its theoretical
properties. We then present two implementations of our technique:
k-inductor, a verifier for C programs built on top of the CBMC model
checker, and k-Boogie, an extension of the Boogie tool. Our experiments,
using a large set of benchmarks, demonstrate that our k-induction
technique frequently allows program verification to succeed using
significantly weaker loop invariants than are required with the standard
inductive invariant approach.