Verifying Array Manipulating Programs with Full-Program Induction

Abstract

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 loops) directly via the program parameter N . Significantly, this does not require generation or use of loop-specific invariants. We have developed a prototype tool V ajra to assess the efficacy of our technique. We demonstrate the performance of V ajra vis-a-vis several state-of-the-art tools on a set of array manipulating benchmarks.