HaliVer: Deductive Verification and Scheduling Languages Join Forces

Lars B. van den Haak; Anton Wijs; Marieke Huisman; Mark van den Brand

doi:10.48550/arXiv.2401.10778

HaliVer: Deductive Verification and Scheduling Languages Join Forces

Lars B. van den Haak
, Anton Wijs
, Marieke Huisman
, Mark van den Brand

Research output: Working paper › Preprint › Academic

62 Downloads (Pure)

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.

Original language	Undefined
Publisher	ArXiv.org
DOIs	https://doi.org/10.48550/arXiv.2401.10778
Publication status	Published - 19 Jan 2024

Keywords

cs.LO
cs.PL

Access to Document

10.48550/arXiv.2401.10778Licence: CC BY

Article-v1Final published version, 402 KBLicence: CC BY

HaliVer: Deductive Verification and Scheduling Languages Join Forces
Haak, L. B. V. D., Wijs, A., Huisman, M. & Brand, M. V. D., 5 Apr 2024, Tools and Algorithms for the Construction and Analysis of Systems : 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings. Finkbeiner, B. & Kovács, L. (eds.). p. 71-89 19 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Open Access
File
2 Link opens in a new tab Citations (Scopus)

137 Downloads (Pure)

Cite this

@techreport{7fe5b288ea534679b0dc9e778b2af216,

title = "HaliVer: Deductive Verification and Scheduling Languages Join Forces",

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 \textbackslash{}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. ",

keywords = "cs.LO, cs.PL",

author = "Haak, \{Lars B. van den\} and Anton Wijs and Marieke Huisman and Brand, \{Mark van den\}",

year = "2024",

month = jan,

day = "19",

doi = "10.48550/arXiv.2401.10778",

language = "Undefined",

publisher = "ArXiv.org",

type = "WorkingPaper",

institution = "ArXiv.org",

}

TY - UNPB

T1 - HaliVer

T2 - Deductive Verification and Scheduling Languages Join Forces

AU - Haak, Lars B. van den

AU - Wijs, Anton

AU - Huisman, Marieke

AU - Brand, Mark van den

PY - 2024/1/19

Y1 - 2024/1/19

N2 - 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.

AB - 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.

KW - cs.LO

KW - cs.PL

U2 - 10.48550/arXiv.2401.10778

DO - 10.48550/arXiv.2401.10778

M3 - Preprint

BT - HaliVer

PB - ArXiv.org

ER -