HaliVer: Deductive Verification and Scheduling Languages Join Forces

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

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

18 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 an 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 languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication30th 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
EditorsBernd Finkbeiner, Laura Kovács
Pages71-89
Number of pages19
ISBN (Electronic)978-3-031-57256-2
DOIs
Publication statusPublished - 5 Apr 2024
Event30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024 - Luxembourg City, Luxembourg
Duration: 6 Apr 202411 Apr 2024
Conference number: 30

Conference

Conference30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024
Abbreviated titleTACAS 2024
Country/TerritoryLuxembourg
CityLuxembourg City
Period6/04/2411/04/24

Keywords

  • 2024 OA procedure

Fingerprint

Dive into the research topics of 'HaliVer: Deductive Verification and Scheduling Languages Join Forces'. Together they form a unique fingerprint.

Cite this