{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:20:04Z","timestamp":1784830804675,"version":"3.55.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031572555","type":"print"},{"value":"9783031572562","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T00:00:00Z","timestamp":1712275200000},"content-version":"vor","delay-in-days":95,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The <jats:sc>HaliVer<\/jats:sc> tool integrates deductive verification into the popular scheduling language <jats:sc>Halide<\/jats:sc>, used for image processing pipelines and array computations. <jats:sc>HaliVer<\/jats:sc> uses <jats:sc>VerCors<\/jats:sc>, a separation logic-based verifier, to verify the correctness of (1) the <jats:sc>Halide<\/jats:sc> algorithms and (2) the optimised parallel code produced by <jats:sc>Halide<\/jats:sc> 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 <jats:sc>Halide<\/jats:sc> algorithms, using all but one of the essential scheduling directives available in <jats:sc>Halide<\/jats:sc>. Without annotation effort, <jats:sc>HaliVer<\/jats:sc> proves memory safety in almost all programs. With annotations <jats:sc>HaliVer<\/jats:sc>, additionally, proves functional correctness properties. We show that the approach is viable and reduces the manual annotation effort by an order of magnitude.<\/jats:p>","DOI":"10.1007\/978-3-031-57256-2_4","type":"book-chapter","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T08:03:04Z","timestamp":1712217784000},"page":"71-89","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["$${\\textsc {HaliVer}}$$: Deductive Verification and Scheduling Languages Join Forces"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0330-5016","authenticated-orcid":false,"given":"Lars B.","family":"van den Haak","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2071-9624","authenticated-orcid":false,"given":"Anton","family":"Wijs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4467-072X","authenticated-orcid":false,"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3529-6182","authenticated-orcid":false,"given":"Mark","family":"van den Brand","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,4,5]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1) (2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:2)2015","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Bacon, D., Graham, S., Sharp, O.: Compiler Transformations for High-Performance Computing. ACM Computing Surveys 26(4), 345\u2013420 (1994). https:\/\/doi.org\/10.1145\/197405.197406","DOI":"10.1145\/197405.197406"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Baghdadi, R., Ray, J., Romdhane, M.B., Sozzo, E.D., Akkas, A., Zhang, Y., Suriana, P., Kamil, S., Amarasinghe, S.P.: Tiramisu: A Polyhedral Compiler for Expressing Fast and Portable Code. In: CGO. pp. 193\u2013205. IEEE (2019). https:\/\/doi.org\/10.1109\/CGO.2019.8661197","DOI":"10.1109\/CGO.2019.8661197"},{"key":"4_CR4","doi-asserted-by":"publisher","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors Tool Set: Verification of Parallel and Concurrent Software. In: Polikarpova, N., Schneider, S. (eds.) Integr. Form. Methods. pp. 102\u2013110. Lecture Notes in Computer Science, Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL. pp. 259\u2013270 (2005). https:\/\/doi.org\/10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"key":"4_CR6","unstructured":"Chame, C.C.J., Hall, M.: CHiLL: A framework for composing high-level loop transformations. 08-897, University of Southern California (2008)"},{"key":"4_CR7","unstructured":"Chen, T., Moreau, T., Jiang, Z., Zheng, L., Yan, E., Cowan, M., Shen, H., Wang, L., Hu, Y., Ceze, L., Guestrin, C., Krishnamurthy, A.: TVM: An Automated End-to-End Optimizing Compiler for Deep Learning. In: 13th USENIX Symp. Oper. Syst. Des. Implement. OSDI 18. pp. 578\u2013594. USENIX Association, USA (2018)"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Hagedorn, B., Elliott, A.S., Barthels, H., Bodik, R., Grover, V.: Fireiron: A Data-Movement-Aware Scheduling Language for GPUs. In: Proc. ACM Int. Conf. Parallel Archit. Compil. Tech. pp. 71\u201382. ACM, Virtual Event GA USA (Sep 2020). https:\/\/doi.org\/10.1145\/3410463.3414632","DOI":"10.1145\/3410463.3414632"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools. In: Computing and Software Science - State of the Art and Perspectives. LNCS, vol. 10000, pp. 345\u2013373. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Hijma, P., Heldens, S., Sclocco, A., van Werkhoven, B., Bal, H.: Optimization Techniques for GPU Programming. ACM Computing Surveys 55(11), 239:1\u2013239:81 (2023). https:\/\/doi.org\/10.1145\/3570638","DOI":"10.1145\/3570638"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Kowarschik, M., Wei\u00df, C.: An Overview of Cache Optimization Techniques and Cache-Aware Numerical Algorithms. In: Algorithms for Memory Hierarchies. LNCS, vol.\u00a02625, pp. 213\u2013232. Springer (2003). https:\/\/doi.org\/10.1007\/3-540-36574-5_10","DOI":"10.1007\/3-540-36574-5_10"},{"key":"4_CR12","unstructured":"Leijen, D.: Division and modulus for computer scientists (July 2003), https:\/\/www.microsoft.com\/en-us\/research\/publication\/division-and-modulus-for-computer-scientists\/, short note about division definitions in programming languages"},{"key":"4_CR13","doi-asserted-by":"publisher","unstructured":"Leiserson, C.E., Thompson, N.C., Emer, J.S., Kuszmaul, B.C., Lampson, B.W., Sanchez, D., Schardl, T.B.: There\u2019s plenty of room at the top: What will drive computer performance after Moore\u2019s law? Science 368(6495) (2020). https:\/\/doi.org\/10.1126\/science.aam9744","DOI":"10.1126\/science.aam9744"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43(4), 363\u2013446 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9155-4","DOI":"10.1007\/s10817-009-9155-4"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Liu, A., Bernstein, G.L., Chlipala, A., Ragan-Kelley, J.: Verified tensor-program optimization via high-level scheduling rewrites. Proc. ACM Program. Lang. 6(POPL), 55:1\u201355:28 (Jan 2022). https:\/\/doi.org\/10.1145\/3498717","DOI":"10.1145\/3498717"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.: Viper - a verification infrastructure for permission-based reasoning. In: VMCAI (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Namjoshi, K.S., Singhania, N.: Loopy: Programmable and formally verified loop transformations. In: International Static Analysis Symposium. pp. 383\u2013402. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-53413-7_19","DOI":"10.1007\/978-3-662-53413-7_19"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Namjoshi, K.S., Xue, A.: A Self-certifying Compilation Framework for WebAssembly. In: International Conference on Verification, Model Checking, and Abstract Interpretation. pp. 127\u2013148. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_7","DOI":"10.1007\/978-3-030-67067-2_7"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"Newcomb, J.L., Adams, A., Johnson, S., Bodik, R., Kamil, S.: Verifying and Improving Halide\u2019s Term Rewriting System with Program Synthesis. Proc. ACM Program. Lang. 4(OOPSLA), 166:1\u2013166:28 (Nov 2020). https:\/\/doi.org\/10.1145\/3428234","DOI":"10.1145\/3428234"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"O\u2019Connor, L., Chen, Z., Rizkallah, C., Jackson, V., Amani, S., Klein, G., Murray, T., Sewell, T., Keller, G.: Cogent: Uniqueness Types and Certifying Compilation. Journal of Functional Programming 31(e25), 1\u201366 (2021). https:\/\/doi.org\/10.1017\/S095679682100023X","DOI":"10.1017\/S095679682100023X"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"de\u00a0Putter, S., Wijs, A.: Verifying a verifier: on the formal correctness of an LTS transformation verification technique. In: FASE. pp. 383\u2013400. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49665-7_23","DOI":"10.1007\/978-3-662-49665-7_23"},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Ragan-Kelley, J., Adams, A., Sharlet, D., Barnes, C., Paris, S., Levoy, M., Amarasinghe, S., Durand, F.: Halide: Decoupling algorithms from schedules for high-performance image processing. Commun. ACM 61(1), 106\u2013115 (Dec 2017).https:\/\/doi.org\/10.1145\/3150211","DOI":"10.1145\/3150211"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Ragan-Kelley, J., Barnes, C., Adams, A., Paris, S., Durand, F., Amarasinghe, S.: Halide: A Language and Compiler for Optimizing Parallelism, Locality, and Recomputation in Image Processing Pipelines. SIGPLAN Not. 48(6), 519\u2013530 (Jun 2013). https:\/\/doi.org\/10.1145\/2499370.2462176","DOI":"10.1145\/2499370.2462176"},{"key":"4_CR24","unstructured":"Reinking, A., Bernstein, G., Ragan-Kelley, J.: Formal Semantics for the Halide Language. Master\u2019s thesis, EECS Department, University of California, Berkeley (2020, May)"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Safari, M., Huisman, M.: Formal verification of parallel stream compaction and summed-area table algorithms. In: International Colloquium on Theoretical Aspects of Computing. pp. 181\u2013199. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-64276-1_10","DOI":"10.1007\/978-3-030-64276-1_10"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Safari, M., Oortwijn, W., Joosten, S., Huisman, M.: Formal Verification of Parallel Prefix Sum. In: Lee, R., Jha, S., Mavridou, A. (eds.) NASA Form. Methods. pp. 170\u2013186. Lecture Notes in Computer Science, Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_10","DOI":"10.1007\/978-3-030-55754-6_10"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Sakar, \u00d6., Safari, M., Huisman, M., Wijs, A.: Alpinist: An Annotation-Aware GPU Program Optimizer. In: TACAS, LNCS, vol. 13244, pp. 332\u2013352. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_18","DOI":"10.1007\/978-3-030-99527-0_18"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Yang, M., Baghdadi, R., Kamil, S., Shun, J., Amarasinghe, S.P.: GraphIt: a high-performance graph DSL. Proc. ACM Program. Lang. 2(OOPSLA), 1\u201330 (2018). https:\/\/doi.org\/10.1145\/3276491","DOI":"10.1145\/3276491"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57256-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T08:06:47Z","timestamp":1712218007000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57256-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572555","9783031572562"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57256-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"5 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}