Full-Program Induction: Verifying Array Programs sans Loop Invariants

TL;DR

The paper introduces full-program induction, a novel verification method that proves safety properties of array programs without loop invariants by inducting over the entire program structure.

Contribution

It presents a new verification technique that inducts over entire array programs directly, eliminating the need for loop invariants and transforming programs to simpler forms.

Findings

Vajra outperforms several state-of-the-art tools on array benchmarks.

The technique effectively reduces complex programs to simpler or loop-free forms.

Full-program induction successfully verifies properties without loop invariants.

Abstract

Arrays are commonly used in a variety of software to store and process data in loops. Automatically proving safety properties of such programs that manipulate arrays is challenging. We present a novel verification technique, called full-program induction, 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$. The technique performs non-trivial transformations of the given program and pre-conditions during the inductive step. The transformations assist in effectively reducing the assertion checking problem by transforming a program with multiple loops to a program which has fewer and simpler loops or is loop-free. Significantly, full-program induction does not require generation or use of loop-specific invariants. To assess the efficacy of our technique, we have developed a prototype tool called Vajra. We demonstrate the performance of Vajra vis-a-vis several state-of-the-art tools on a large set of array manipulating benchmarks from the international software verification competition (SV-COMP) and on several programs inspired by algebraic functions that perform polynomial computations.