Scalable Deductive Verification of Data-Level Parallel Programs

TL;DR

This paper presents scalable techniques for deductive verification of data-parallel programs, significantly reducing verification time and enabling previously infeasible proofs, with implementation in the VerCors verifier.

Contribution

It introduces new expression rewriting and array aliasing techniques, improving scalability and correctness in verifying data-level parallel programs.

Findings

Verification time reduced by up to 150 times

Able to verify previously infeasible results

Techniques proven correct in a theorem prover

Abstract

This paper introduces several techniques that improve the scalability of the deductive verification of data-level programs working on arrays and matrices. First of all, we introduce a technique to rewrite expressions with (nested) quantifiers, so suitable triggers can be generated for these expressions. We have proven this rewrite technique correct in a theorem prover. Second, we make reasoning about potentially overlapping arrays easier, by providing specification constructs to indicate and verify that two arrays are not aliases, or that they are immutable, so they can be modelled as mathematical sequences. All our techniques are implemented in the VerCors program verifier. We illustrate how our techniques improve scalability through a large number of experiments. Using our techniques on a set of typical GPU kernels, we achieve a reduction of verification time by, on average, a factor of 9, with outliers being up to 150 times faster. Additionally, applying these techniques to earlier experiments and an earlier case study of a radio telescope pipeline permitted the verification of results which were previously unobtainable and significantly reduced the verification time.