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.