{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:05:20Z","timestamp":1742918720326,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031773815"},{"type":"electronic","value":"9783031773822"}],"license":[{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-77382-2_11","type":"book-chapter","created":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T19:26:49Z","timestamp":1732562809000},"page":"182-199","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Deductive Verification of\u00a0SYCL in\u00a0VerCors"],"prefix":"10.1007","author":[{"given":"Ellen","family":"Wittingen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4467-072X","authenticated-orcid":false,"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3457-5446","authenticated-orcid":false,"given":"\u00d6mer","family":"\u015eakar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,26]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Aktemur, B., Metzger, M., Saiapova, N., Strasuns, M.: Debugging SYCL programs on heterogeneous Intel\u00ae architectures. In: Proceedings of the International Workshop on OpenCL, pp. 1\u201310 (2020)","DOI":"10.1145\/3388333.3388646"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multi-threaded Java programs. Logic. Methods Comput. Sci. 11(1), 2 (2015). https:\/\/doi.org\/10.2168\/LMCS-11(1:2)2015","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-22969-0_5","volume-title":"Software Engineering and Formal Methods","author":"A Amighi","year":"2015","unstructured":"Amighi, A., Darabi, S., Blom, S., Huisman, M.: Specification and verification of atomic operations in GPGPU programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 69\u201383. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22969-0_5"},{"key":"11_CR4","unstructured":"Artima. ScalaTest support in the IntelliJ Scala plugin. https:\/\/www.scalatest.org\/user_guide\/using_scalatest_with_intellij. Accessed 15 Apr 2024"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA 2012), pp. 113\u2013132. Association for Computing Machinery (2012). https:\/\/doi.org\/10.1145\/2384616.2384625","DOI":"10.1145\/2384616.2384625"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","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.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Blom, S., Darabi, S., Huisman, M., Safari, M.: Correct program parallelisations. Int. J. Softw. Tools Technol. Transfer 23(5), 741\u2013763 (2021). https:\/\/doi.org\/10.1007\/s10009-020-00601-z","DOI":"10.1007\/s10009-020-00601-z"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Blom, S., Huisman, M., Mihelil, M.: Specification and verification of GPGPU programs. Sci. Comput. Program. 95, 376\u2013388 (2014). Special Section: ACM SAC-SVT 2013 + Bytecode 2013","DOI":"10.1016\/j.scico.2014.03.013"},{"key":"11_CR9","doi-asserted-by":"publisher","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.: Permission accounting in separation logic. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 259\u2013270 (2005). https:\/\/doi.org\/10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"key":"11_CR10","unstructured":"Codeplay Software Ltd. Introduction to SYCL. https:\/\/tech.io\/playgrounds\/48226\/introduction-to-sycl\/hello-world. Accessed 15 Apr 2024"},{"key":"11_CR11","unstructured":"Codeplay Software Ltd. SYCL Guide. https:\/\/developer.codeplay.com\/products\/computecpp\/ce\/2.11.0\/guides\/sycl-guide. Accessed 15 Apr 2024"},{"key":"11_CR12","unstructured":"Codeplay Software Ltd. SYCL Academy on GitHub (2024). https:\/\/github.com\/codeplaysoftware\/syclacademy"},{"key":"11_CR13","unstructured":"Darabi, S.: Verification of program parallelization. Ph.D. thesis, University of Twente (2018). iPA Dissertation Series No. 2018-02 IDS PhD. Thesis Series No. 18-458"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS, 29 March\u20136 April 2008, Proceedings 14. pp. 337\u2013340. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"11_CR15","unstructured":"Intel. Explore SYCL with Samples from Intel (2023). https:\/\/www.intel.com\/content\/www\/us\/en\/docs\/oneapi\/code-samples-dpcpp\/2023-1\/overview.html"},{"key":"11_CR16","unstructured":"JetBrains s.r.o. IntelliJ IDEA the Leading Java and Kotlin IDE. https:\/\/www.jetbrains.com\/idea\/. Accessed 15 Apr 2024"},{"key":"11_CR17","unstructured":"Khronos\u00ae OpenCL Working Group. OpenCL\u2122 Specification (2024). https:\/\/registry.khronos.org\/OpenCL\/specs\/3.0-unified\/pdf\/OpenCL_API.pdf"},{"key":"11_CR18","unstructured":"Khronos\u00ae SYCL\u2122 Working Group. SYCL\u2122 2020 Specification (revision 7) (2023). https:\/\/registry.khronos.org\/SYCL\/specs\/sycl-2020\/pdf\/sycl-2020.pdf. Compiled from https:\/\/github.com\/KhronosGroup\/SYCL-Docs\/tree\/SYCL-2020\/final-rev7"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Lal, S., et al.: SYCL-Bench: a versatile cross-platform benchmark suite for heterogeneous computing. In: Malawski, M., Rzadca, K. (eds.) Euro-Par 2020. LNCS, vol. 12247, pp. 629\u2013644. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-57675-2_39","DOI":"10.1007\/978-3-030-57675-2_39"},{"key":"11_CR20","doi-asserted-by":"publisher","unstructured":"Lal, S., et al.: SYCL-Bench: a versatile single-source benchmark suite for heterogeneous computing. In: Proceedings of the International Workshop on OpenCL (IWOCL 20). Association for Computing Machinery (2020). https:\/\/doi.org\/10.1145\/3388333.3388669","DOI":"10.1145\/3388333.3388669"},{"key":"11_CR21","unstructured":"Leavens, G.T., et al.: JML reference manual, DRAFT, Rev. 2344. http:\/\/www.jmlspecs.org\/refman\/jmlrefman.pdf"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 187\u2013196 (2010)","DOI":"10.1145\/1882291.1882320"},{"key":"11_CR23","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":"11_CR24","unstructured":"NVIDIA. CUDA Toolkit Documentation 12.1 (2024). https:\/\/docs.nvidia.com\/cuda\/index.html"},{"key":"11_CR25","doi-asserted-by":"publisher","unstructured":"Reinders, J., Ashbaugh, B., Brodman, J., Kinsner, M., Pennycook, J., Tian, X.: Data Parallel C++. Apress (2021). https:\/\/doi.org\/10.1007\/978-1-4842-5574-2","DOI":"10.1007\/978-1-4842-5574-2"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Safari, M., Huisman, M.: Formal verification of parallel prefix sum and stream compaction algorithms in CUDA. Theor. Comput. Sci. 912, 81\u201398 (2022). https:\/\/doi.org\/10.1016\/j.tcs.2022.02.027","DOI":"10.1016\/j.tcs.2022.02.027"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Siegel, H.J., Antonio, J.K., Metzger, R.C., Tan, M., Li, Y.A.: Heterogeneous Computing. ECE Technical Reports, p.\u00a0206 (1994)","DOI":"10.1117\/12.200804"},{"key":"11_CR28","unstructured":"UTwente FMT Group. VerCors\u2019 Source Code on GitHub (2024). https:\/\/github.com\/utwente-fmt\/vercors"},{"key":"11_CR29","unstructured":"Wittingen, E.: Deductive verification for SYCL. Master\u2019s thesis (2024). http:\/\/essay.utwente.nl\/97976\/"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Xing, Y., Huang, B., Gupta, A., Malik, S.: A formal instruction-level GPU model for scalable verification. In: 2018 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 2018 - Digest of Technical Papers. Institute of Electrical and Electronics Engineers Inc. (2018). https:\/\/doi.org\/10.1145\/3240765.3240771","DOI":"10.1145\/3240765.3240771"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Zahran, M.: Heterogeneous computing: here to stay: hardware and software perspectives. Queue 14(6), 31\u201342 (2016). https:\/\/doi.org\/10.1145\/3028687.3038873","DOI":"10.1145\/3028687.3038873"},{"key":"11_CR32","doi-asserted-by":"publisher","unstructured":"Zheng, M., Rogers, M.S., Luo, Z., Dwyer, M.B., Siegel, S.F.: CIVL: formal verification of parallel programs. In: 2015 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 830\u2013835 (2015). https:\/\/doi.org\/10.1109\/ASE.2015.99","DOI":"10.1109\/ASE.2015.99"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Sakar, \u00d6., Wittingen, E., Huisman, M.: Artifact for paper (Deductive verification of SYCL in VerCors) (2024). https:\/\/doi.org\/10.4121\/45d37292-cce5-4fb7-8d4e-a1b32cfa3028","DOI":"10.4121\/45d37292-cce5-4fb7-8d4e-a1b32cfa3028"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77382-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T20:02:56Z","timestamp":1732564976000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77382-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,26]]},"ISBN":["9783031773815","9783031773822"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77382-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,26]]},"assertion":[{"value":"26 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aveiro","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":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}