HALIVER: Deductive Verification and Scheduling Languages Join Forces

Lars B. van den Haak (Corresponding author), Anton Wijs, Marieke Huisman, Mark van den Brand

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

1 Citation (Scopus)

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, Part III
EditorsBernd Finkbeiner, Laura Kovács
Place of PublicationCham
PublisherSpringer
Pages71-89
Number of pages19
ISBN (Electronic)978-3-031-57256-2
ISBN (Print)978-3-031-57255-5
DOIs
Publication statusPublished - 5 Apr 2024
Event30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024 - Luxembourg City, Luxembourg
Duration: 6 Apr 202411 Apr 2024

Publication series

NameLecture Notes in Computer Science (LNCS)
Volume14572
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, which was held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024
Country/TerritoryLuxembourg
CityLuxembourg City
Period6/04/2411/04/24

Keywords

  • Deductive verification
  • Program correctness
  • Scheduling language

Fingerprint

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

Cite this