Verifying Array Manipulating Programs with Full-Program Induction

Supratik Chakraborty, Ashutosh Gupta, Divyesh Unadkat

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. In…