@inproceedings{Haak24,
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 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.",
keywords = "2024 OA procedure",
author = "{van den Haak}, Lars and Anton Wijs and Marieke Huisman and {van den Brand}, Mark",
year = "2024",
month = apr,
day = "5",
doi = "10.1007/978-3-031-57256-2_4",
language = "English",
isbn = "978-3-031-57255-5",
pages = "71--89",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
note = "30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, TACAS 2024 ; Conference date: 06-04-2024 Through 11-04-2024",

}

{"_id":"uxcjNczk4vCN4C8aA","bibbaseid":"vandenhaak-wijs-huisman-vandenbrand-haliverdeductiveverificationandschedulinglanguagesjoinforces-2024","author_short":["van den Haak , L.","Wijs, A.","Huisman, M.","van den Brand , M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","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 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.","keywords":"2024 OA procedure","author":[{"propositions":["van den Haak"],"lastnames":[],"firstnames":["Lars"],"suffixes":[]},{"firstnames":["Anton"],"propositions":[],"lastnames":["Wijs"],"suffixes":[]},{"firstnames":["Marieke"],"propositions":[],"lastnames":["Huisman"],"suffixes":[]},{"propositions":["van den Brand"],"lastnames":[],"firstnames":["Mark"],"suffixes":[]}],"year":"2024","month":"April","day":"5","doi":"10.1007/978-3-031-57256-2_4","language":"English","isbn":"978-3-031-57255-5","pages":"71–89","booktitle":"Tools and Algorithms for the Construction and Analysis of Systems","note":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, TACAS 2024 ; Conference date: 06-04-2024 Through 11-04-2024","bibtex":"@inproceedings{Haak24,\ntitle = \"HaliVer: Deductive Verification and Scheduling Languages Join Forces\",\nabstract = \"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.\",\nkeywords = \"2024 OA procedure\",\nauthor = \"{van den Haak}, Lars and Anton Wijs and Marieke Huisman and {van den Brand}, Mark\",\nyear = \"2024\",\nmonth = apr,\nday = \"5\",\ndoi = \"10.1007/978-3-031-57256-2_4\",\nlanguage = \"English\",\nisbn = \"978-3-031-57255-5\",\npages = \"71--89\",\nbooktitle = \"Tools and Algorithms for the Construction and Analysis of Systems\",\nnote = \"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, TACAS 2024 ; Conference date: 06-04-2024 Through 11-04-2024\",\n\n}\n\n","author_short":["van den Haak , L.","Wijs, A.","Huisman, M.","van den Brand , M."],"key":"Haak24","id":"Haak24","bibbaseid":"vandenhaak-wijs-huisman-vandenbrand-haliverdeductiveverificationandschedulinglanguagesjoinforces-2024","role":"author","urls":{},"keyword":["2024 OA procedure"],"metadata":{"authorlinks":{}},"html":""},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/utwente-fmt/vercors-web/master/static/references.bib","dataSources":["cCvCnPTRQYq3qPe9y"],"keywords":["2024 oa procedure"],"search_terms":["haliver","deductive","verification","scheduling","languages","join","forces","van den haak ","wijs","huisman","van den brand "],"title":"HaliVer: Deductive Verification and Scheduling Languages Join Forces","year":2024}