Verifying Array Manipulating Programs with Full-Program Induction

We present a full-program induction technique for proving (a sub-class of) quantified as well as quantifier-free properties of programs manipulating arrays of parametric size N . Instead of inducting over individual loops, our technique inducts over the entire program (possibly containing multiple l... View More