{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:03:34Z","timestamp":1784793814885,"version":"3.55.0"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325181","type":"print"},{"value":"9783032325198","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This paper introduces several techniques that improve the scalability of the deductive verification of data-level parallel programs working on arrays and matrices. First of all, we introduce a technique to rewrite expressions with (nested) quantifiers, so suitable triggers can be generated for these expressions. We have proven this rewrite technique correct using a theorem prover. Second, we make reasoning about potentially overlapping arrays easier, by providing specification constructs to indicate and verify that two arrays are not aliases, or that they are immutable, so they can be modelled as mathematical sequences. All our techniques are implemented in the\n                    <jats:sc>VerCors<\/jats:sc>\n                    program verifier. We illustrate how the combination of our techniques improves scalability via a large number of experiments. Using our techniques on a set of typical GPU kernels, we achieve a reduction of verification time by, on average, a factor of 9, with outliers being up to 150 times faster. Additionally, applying these techniques to earlier experiments and an earlier case study of a radio telescope pipeline permitted to obtain verification results that were previously either unobtainable or only in a significantly longer verification time.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32519-8_5","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:42Z","timestamp":1784791062000},"page":"90-112","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Scalable Deductive Verification of\u00a0Data-Level Parallel Programs"],"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"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Armborst, L., et al.: The VerCors verifier: a progress report. In: CAV. LNCS, vol. 14682, pp. 3\u201318. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65630-9_1","DOI":"10.1007\/978-3-031-65630-9_1"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-29737-3_22","volume-title":"Euro-Par 2011: Parallel Processing Workshops","author":"C Bertolli","year":"2012","unstructured":"Bertolli, C., Betts, A., Mudalige, G., Giles, M., Kelly, P.: Design and performance of the op2 library for unstructured mesh applications. In: Alexander, M., et al. (eds.) Euro-Par 2011. LNCS, vol. 7155, pp. 191\u2013200. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29737-3_22"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Bierhoff, K.: Automated program verification made SYMPLAR: symbolic permissions for lightweight automated reasoning. In: Proceedings of the 10th SIGPLAN Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, pp. 19\u201332. ACM (2011). https:\/\/doi.org\/10.1145\/2048237.2048242","DOI":"10.1145\/2048237.2048242"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1016\/j.scico.2014.03.013","volume":"95","author":"S Blom","year":"2014","unstructured":"Blom, S., Huisman, M., Mihel\u010di\u0107, M.: Specification and verification of GPGPU programs. Sci. Comput. Program. 95, 376\u2013388 (2014). https:\/\/doi.org\/10.1016\/j.scico.2014.03.013","journal-title":"Sci. Comput. Program."},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-28644-8_2","volume-title":"CONCUR 2004 - Concurrency Theory","author":"S Brookes","year":"2004","unstructured":"Brookes, S.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 16\u201334. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-28644-8_2"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-662-54434-1_10","volume-title":"Programming Languages and Systems","author":"A Chargu\u00e9raud","year":"2017","unstructured":"Chargu\u00e9raud, A., Pottier, F.: Temporary read-only permissions for separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 260\u2013286. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_10"},{"issue":"3","key":"5_CR7","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005). https:\/\/doi.org\/10.1145\/1066100.1066102","journal-title":"J. ACM"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Eilers, M., Schwerhoff, M., Summers, A.J., M\u00fcller, P.: Fifteen years of viper. In: CAV, pp. 107\u2013123. Springer-Verlag, Berlin (2025). https:\/\/doi.org\/10.1007\/978-3-031-98668-0_5","DOI":"10.1007\/978-3-031-98668-0_5"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Grewe, D., Lokhmotov, A.: Automatically generating and tuning GPU code for sparse matrix-vector multiplication from a high-level representation. In: Proceedings of the 4th Workshop on General Purpose Processing on Graphics Processing Units (GPGPU). ACM (2011). https:\/\/doi.org\/10.1145\/1964179.1964196","DOI":"10.1145\/1964179.1964196"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-642-03013-0_24","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"C Haack","year":"2009","unstructured":"Haack, C., Poll, E.: Type-based object immutability with flexible initialization. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 520\u2013545. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03013-0_24"},{"key":"5_CR11","unstructured":"van\u00a0den Haak, L.B., Wijs, A., Huisman, M.: Scalable deductive verification of data-level parallel programs (2026). https:\/\/arxiv.org\/abs\/2605.13616"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-030-63461-2_9","volume-title":"Integrated Formal Methods","author":"LB van den Haak","year":"2020","unstructured":"van den Haak, L.B., Wijs, A., van den Brand, M., Huisman, M.: Formal methods for GPGPU programming: is the demand met? In: Dongol, B., Troubitsyna, E. (eds.) IFM 2020. LNCS, vol. 12546, pp. 160\u2013177. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63461-2_9"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"van\u00a0den Haak, L.B., Wijs, A.J., Huisman, M., van den Brand, M.G.J.: HaliVer: deductive verification and scheduling languages join forces. In: TACAS. LNCS, vol. 14572, pp. 71\u201389. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_4","DOI":"10.1007\/978-3-031-57256-2_4"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"van\u00a0den Haak, L.B., Wijs, A.J., Huisman, M., van den Brand, M.G.J.: Verifying a\u00a0radio telescope pipeline using HaliVer: solving nonlinear and\u00a0quantifier challenges. In: FMICS. LNCS, vol. 14952, pp. 152\u2013169. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-68150-9_9","DOI":"10.1007\/978-3-031-68150-9_9"},{"issue":"12","key":"5_CR15","doi-asserted-by":"publisher","first-page":"1170","DOI":"10.1145\/7902.7903","volume":"29","author":"WD Hillis","year":"1986","unstructured":"Hillis, W.D., Steele, G.L.: Data parallel algorithms. Commun. ACM 29(12), 1170\u20131183 (1986). https:\/\/doi.org\/10.1145\/7902.7903","journal-title":"Commun. ACM"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Le, Q., Ngiam, J., Coates, A., Lahiri, A., Prochnow, B., Ng, A.: On Optimization methods for deep learning. In: Proceedings of the 28th International Conference on Machine Learning (ICML), pp. 265\u2013272. Omnipress (2011). https:\/\/doi.org\/10.5555\/3104482.3104516","DOI":"10.5555\/3104482.3104516"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: CAV. LNCS, vol.\u00a09779, pp. 361\u2013381. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_20","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Liu, X., Tan, S., Wang, H.: Parallel statistical analysis of analog circuits by GPU-accelerated graph-based approach. In: Proceedings of the 2012 Conference and Exhibition on Design, Automation & Test in Europe (DATE), pp. 852\u2013857. IEEE (2012). https:\/\/doi.org\/10.1109\/DATE.2012.6176615","DOI":"10.1109\/DATE.2012.6176615"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-319-41528-4_22","volume-title":"Computer Aided Verification","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Automatic verification of iterated separating conjunctions using symbolic execution. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 405\u2013425. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_22"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Nugteren, C.: CLBlast: a tuned OpenCL BLAS library. In: Proceedings of the International Workshop on OpenCL (WOCL), pp. 1\u201310. ACM (2018). https:\/\/doi.org\/10.1145\/3204919.3204924","DOI":"10.1145\/3204919.3204924"},{"issue":"1","key":"5_CR24","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/3150211","volume":"61","author":"J Ragan-Kelley","year":"2017","unstructured":"Ragan-Kelley, J., et al.: Halide: decoupling algorithms from schedules for high-performance image processing. Commun. ACM 61(1), 106\u2013115 (2017). https:\/\/doi.org\/10.1145\/3150211","journal-title":"Commun. ACM"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Schwerhoff, M.H.: Advancing automated, permission-based program verification using symbolic execution. Doctoral Thesis, ETH Zurich (2016). https:\/\/doi.org\/10.3929\/ethz-a-010835519","DOI":"10.3929\/ethz-a-010835519"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1007\/978-3-642-32820-6_85","volume-title":"Euro-Par 2012 Parallel Processing","author":"S Wienke","year":"2012","unstructured":"Wienke, S., Springer, P., Terboven, C., an Mey, D.: OpenACC \u2014 first experiences with real-world applications. In: Kaklamanis, C., Papatheodorou, T., Spirakis, P.G. (eds.) Euro-Par 2012. LNCS, vol. 7484, pp. 859\u2013870. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32820-6_85"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-642-31759-0_9","volume-title":"Model Checking Software","author":"AJ Wijs","year":"2012","unstructured":"Wijs, A.J., Bo\u0161na\u010dki, D.: Improving GPU sparse matrix-vector multiplication for probabilistic model checking. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 98\u2013116. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31759-0_9"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-030-81685-8_17","volume-title":"Computer Aided Verification","author":"FA Wolf","year":"2021","unstructured":"Wolf, F.A., Arquint, L., Clochard, M., Oortwijn, W., Pereira, J.C., M\u00fcller, P.: Gobra: modular specification and\u00a0verification of go programs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 367\u2013379. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_17"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Zhou, K., et al.: Linear layouts: robust code generation of efficient tensor computation using F_2. In: Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), vol. 1. pp. 132\u2013146. ACM (2026). https:\/\/doi.org\/10.1145\/3760250.3762221","DOI":"10.1145\/3760250.3762221"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32519-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T07:17:44Z","timestamp":1784791064000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32519-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325181","9783032325198"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32519-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"The data for the experiments (Sect.\u00a0\n                      \n                      ), the\n                      Lean\n                      proof (Sect.\u00a0\n                      \n                      ), and the version of the\n                      VerCors\n                      tool used in this paper can be found in an accompanying artefact at\n                      \n                      .","order":2,"name":"Ethics","label":"Data-Availability Statement","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}