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.

翻译：HaliVer工具将演绎验证集成到流行的调度语言Halide中，该语言用于图像处理流水线和数组计算。HaliVer使用基于分离逻辑的验证器Vercors，验证（1）Halide算法和（2）当对算法应用优化调度时由Halide生成的优化并行代码的正确性。这使得能够证明复杂优化代码的正确性，同时减少提供所需验证注释的工作量。两种方法均使用相同的规范。我们在Halide中除一个外的所有基本调度指令上，对由特征性Halide算法生成的多个优化程序进行了工具评估。在无注释工作量的情况下，HaliVer几乎在所有程序中证明了内存安全性。添加注释后，HaliVer还可证明功能性正确性属性。我们表明该方法可行，并将手动注释工作量降低了一个数量级。