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 lo... View More