HaliVer: Deductive Verification and Scheduling Languages Join Forces

TL;DR

HaliVer addresses the challenge of proving correctness for highly optimised, parallel Halide code by fusing scheduling-language verification with deductive verification via VerCors. It provides two workflows: front-end verification of the algorithm against a single functional specification, and back-end verification of the Halide-generated C code, with automatic generation and transformation of annotations to bridge the two stages. Empirical results show strong memory-safety proofs without user annotations and substantial functional-correctness proofs when annotations are supplied, with annotation effort significantly reduced compared to manual proofs. The approach offers a flexible, extensible path to verify complex, optimised pipelines across scheduling passes and architectures, though it relies on tool limitations of VerCors and SMT solvers that warrant further work.

Abstract

The HaliVer tool integrates deductive verification into the popular scheduling language Halide, used for image processing pipelines and array computations. HaliVer uses Vercors, a separation logic-based verifier, to verify the correctness of (1) the Halide algorithms and (2) the optimised parallel code produced by \halide when an optimisation schedule is applied to the algorithm. This allows proving complex, optimised code correct while reducing the effort to provide the required verification annotations. For both approaches, the same specification is used. We evaluated the tool on several optimised programs generated from characteristic Halide algorithms, using all but one of the essential scheduling directives available in Halide. Without annotation effort, Haliver proves memory safety in almost all programs. With annotations Haliver, additionally, proves functional correctness properties. We show that the approach is viable and reduces the manual annotation effort by an order of magnitude.

Figures (1)

• Figure 1: High level overview of our approach.