{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:20:03Z","timestamp":1784830803823,"version":"3.55.0"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656293","type":"print"},{"value":"9783031656309","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,7,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"vor","delay-in-days":206,"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>This paper gives an overview of the most recent developments on the VerCors verifier. VerCors is a deductive verifier for concurrent software, written in multiple programming languages, where the specifications are written in terms of pre-\/postcondition contracts using permission-based separation logic. In essence, VerCors is a program transformation tool: it translates an annotated program into input for the Viper framework, which is then used as verification back-end. The paper discusses the different programming languages and features for which VerCors provides verification support. It also discusses how the tool internally has been reorganised to become easily extendible, and to improve the connection and interaction with Viper. In addition, we also introduce two tools built on top of VerCors, which support correctness-preserving transformations of verified programs. Finally, we discuss how the VerCors verifier has been used on a range of realistic case studies.<\/jats:p>","DOI":"10.1007\/978-3-031-65630-9_1","type":"book-chapter","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:01:56Z","timestamp":1721858516000},"page":"3-18","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["The VerCors Verifier: A Progress Report"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7565-0954","authenticated-orcid":false,"given":"Lukas","family":"Armborst","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-0240-3305","authenticated-orcid":false,"given":"Pieter","family":"Bos","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0330-5016","authenticated-orcid":false,"given":"Lars B.","family":"van den Haak","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-0002-5638-5945","authenticated-orcid":false,"given":"Robert","family":"Rubbens","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3457-5446","authenticated-orcid":false,"given":"\u00d6mer","family":"\u015eakar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1518-4079","authenticated-orcid":false,"given":"Philip","family":"Tasche","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,25]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M.: In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6. ISBN: 9783319498126","DOI":"10.1007\/978-3-319-49812-6"},{"key":"1_CR2","doi-asserted-by":"publisher","unstructured":"Amighi, A., Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: The VerCors project: setting up basecamp. In: Programming Languages meets Program Verification (PLPV 2012), pp. 71\u201382. ACM (2012). https:\/\/doi.org\/10.1145\/2103776.2103785","DOI":"10.1145\/2103776.2103785"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Amighi, A.: Specification and verification of synchronisation classes in Java: a practical approach. Ph.D. thesis. University of Twente (2018). https:\/\/doi.org\/10.3990\/1.9789036544399","DOI":"10.3990\/1.9789036544399"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Armborst, L., Huisman, M.: Permission-based verification of red-black trees and their merging. In: 2021 IEEE\/ACM 9th International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 111\u2013123 (2021). https:\/\/doi.org\/10.1109\/FormaliSE52586.2021.00017","DOI":"10.1109\/FormaliSE52586.2021.00017"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., et al.: The Prusti project: formal verification for Rust. In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.). NASA Formal Methods, pp. 88\u2013108. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_5. ISBN: 978-3-031-06773-0","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), pp. 3\u201312 (2006). https:\/\/doi.org\/10.1109\/SEFM.2006.27","DOI":"10.1109\/SEFM.2006.27"},{"key":"1_CR7","doi-asserted-by":"publisher","unstructured":"Baudin, P., et al.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64(8), 56\u201368 (2021). https:\/\/doi.org\/10.1145\/3470569","DOI":"10.1145\/3470569"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-030-17462-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Nils Becker","year":"2019","unstructured":"Becker, Nils, M\u00fcller, Peter, Summers, Alexander J..: The axiom profiler: understanding and debugging SMT quantifier instantiations. In: Vojnar, Tom\u00e1\u0161, Zhang, Lijun (eds.) TACAS 2019. LNCS, vol. 11427, pp. 99\u2013116. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17462-0_6"},{"key":"1_CR9","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. ACM (2012). https:\/\/doi.org\/10.1145\/2384616.2384625","DOI":"10.1145\/2384616.2384625"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Bliudze, S., van den Bos, P., Huisman, M., Rubbens, R., Safina, L.: Java-BIP meets VerCors: towards the safety of concurrent software systems in Java. In: Lambers, L., Uchitel, S. (eds.). Fundamental Approaches to Software Engineering, pp. 143\u2013150. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30826-0_8. ISBN: 978-3-031-30826-0","DOI":"10.1007\/978-3-031-30826-0_8"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Bliudze, S., Mavridou, A., Szymanek, R., Zolotukhina, A.: Exogenous coordination of concurrent software components with JavaBIP. In: Software: Practice and Experience, vol. 47, no. 11, pp. 1801\u20131836 (2017). https:\/\/doi.org\/10.1002\/spe.2495. eprint: https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/spe.2495","DOI":"10.1002\/spe.2495"},{"key":"1_CR12","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.) Integrated Formal Methods 2017. LNCS, vol. 10510, pp. 102 \u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"1_CR13","doi-asserted-by":"publisher","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. ISSN: 0167-6423","DOI":"10.1016\/j.scico.2014.03.013"},{"key":"1_CR14","doi-asserted-by":"publisher","unstructured":"Blom, S., Huisman, M.: Witnessing the elimination of magic wands. Int. J. Softw. Tools Technol. Transfer 17(6), 757\u2013781 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0372-3. ISSN: 1433-2787","DOI":"10.1007\/s10009-015-0372-3"},{"key":"1_CR15","unstructured":"Boerman, J.: Formal verification of a sequential SCC algorithm. MA thesis. University of Twente (2023). http:\/\/essay.utwente.nl\/94474\/"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"van den Bos, P., Jongmans, S.: VeyMont: parallelising verified programs instead of verifying parallel programs. In: Chechik, M., Katoen, J., Leucker, M. (eds.) Formal Methods, pp. 321\u2013339. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_19. ISBN: 978-3-031-27481-7","DOI":"10.1007\/978-3-031-27481-7_19"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In: Indagationes Mathematicae (Proceedings), vol. 75, no. 5, pp. 381\u2013392. Elsevier (1972). https:\/\/doi.org\/10.1016\/1385-7258(72)90034-0","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"1_CR18","unstructured":"Budde, N.: Verified version of Kahn\u2019s topological sorting algorithm (2023). https:\/\/github.com\/utwente-fmt\/vercors\/tree\/5e3eb17\/examples\/concepts\/algo\/KahnsTopologicalSort.pvl. Accessed 17 Jan 2024"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Cogumbreiro, T., Lange, J., Rong, D.L.Z., Zicarelli, H.: Checking data-race freedom of GPU kernels, compositionally. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 403\u2013 426. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_19","DOI":"10.1007\/978-3-030-81685-8_19"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Cok, D.: OpenJML: software verification for Java 7 using JML, Open-JDK, and Eclipse. In: Dubois, C., Giannakopoulou, D., Mery, D. (eds.) 1st Workshop on Formal Integrated Development Environment, (F-IDE). EPTCS. 2014, vol. 149, pp. 79\u201392 (2014). https:\/\/doi.org\/10.4204\/EPTCS.149.8","DOI":"10.4204\/EPTCS.149.8"},{"key":"1_CR21","unstructured":"Dross, C., Conchon, S., Paskevich, A.: Reasoning with triggers. Research Report RR-7986. INRIA, p. 29 (2012). https:\/\/inria.hal.science\/hal-00703207"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Eilers, M., M\u00fcller, P.: Nagini: a static verifier for Python. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 596\u2013603. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_33","DOI":"10.1007\/978-3-319-96145-3_33"},{"key":"1_CR23","doi-asserted-by":"publisher","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs met provers. In: Felleisen, M., Gardner, P. (eds.) ESOP. LNCS, vol. 7792, pp. 125\u2013128. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"van den Haak, L., Wijs, A., Huisman, M., van den Brand, M.: HaliVer: deductive verification and scheduling languages join forces. In: TACAS 2024. LNCS. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-57256-2_4"},{"key":"1_CR25","unstructured":"Hollander, J.: Verification of a model checking algorithm in VerCors. MA thesis. University of Twente (2021). http:\/\/essay.utwente.nl\/88268\/"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) Programming Languages and Systems - ESOP 1998. LNCS, vol. 1381, pp. 122\u2013138. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFB0053567","DOI":"10.1007\/BFB0053567"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"IEEE Standards Association. IEEE Std. 1666\u20132011, Open SystemC Language Reference Manual. IEEE Press (2011). https:\/\/doi.org\/10.1109\/IEEESTD.2012.6134619","DOI":"10.1109\/IEEESTD.2012.6134619"},{"key":"1_CR28","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R.: NASA Formal Methods Symposium, pp. 41\u201355. Springer, Cham (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"1_CR29","doi-asserted-by":"publisher","unstructured":"Jongmans, S., van den Bos, P.: A predicate transformer for choreographies - computing preconditions in choreographic programming. In: Sergey, I. (ed.) Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, 2\u20137 April 2022, Proceedings. LNCS, vol. 13240, pp. 520\u2013547. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-030-99336-8_19","DOI":"10.1007\/978-3-030-99336-8_19"},{"key":"1_CR30","doi-asserted-by":"publisher","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018). https:\/\/doi.org\/10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"1_CR31","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: International Symposium on Code Generation and Optimization, 2004. CGO 2004, pp. 75\u201386. IEEE (2004). https:\/\/doi.org\/10.5555\/977395.977673","DOI":"10.5555\/977395.977673"},{"key":"1_CR32","unstructured":"Ledelay, J.: Verification of Distributed Locks: A Case Study. MA thesis. University of Twente (2023). http:\/\/essay.utwente.nl\/95192\/"},{"key":"1_CR33","unstructured":"Leijen, D.: Division and Modulus for Computer Scientists (2003). https:\/\/www.microsoft.com\/en-us\/research\/publication\/divisionand-modulus-for-computer-scientists\/"},{"key":"1_CR34","doi-asserted-by":"publisher","unstructured":"Leino, K.: Accessible software verification with Dafny. IEEE Softw. 34(6), 94\u201397 (2017). https:\/\/doi.org\/10.1109\/MS.2017.4121212","DOI":"10.1109\/MS.2017.4121212"},{"key":"1_CR35","doi-asserted-by":"publisher","unstructured":"Lindholm, L., Nickolls, J., Oberman, S., Montrym, J.: NVIDIA Tesla: a unified graphics and computing architecture. IEEE Micro 28(2), 39\u201355 (2008). https:\/\/doi.org\/10.1109\/MM.2008.31","DOI":"10.1109\/MM.2008.31"},{"key":"1_CR36","doi-asserted-by":"publisher","unstructured":"Montesi, F.: Introduction to Choreographies. Cambridge University Press (2023). https:\/\/doi.org\/10.1017\/9781108981491","DOI":"10.1017\/9781108981491"},{"key":"1_CR37","doi-asserted-by":"publisher","unstructured":"Monti, R.E., Rubbens, R., Huisman, M.: On deductive verification of an industrial concurrent software component with VerCors. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles. ISoLA 2022. LNCS, vol. 13701, pp. 517\u2013534. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-19849-6_29. ISBN: 978-3-031-19849-6","DOI":"10.1007\/978-3-031-19849-6_29"},{"key":"1_CR38","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.: Viper - a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation. VMCAI. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"1_CR39","unstructured":"Nguyen, H.: Formal verification of a red-black tree data structure. MA thesis. University of Twente (2019). http:\/\/essay.utwente.nl\/77569\/"},{"key":"1_CR40","unstructured":"van Oorschot, D.: VCLLVM: A Transformation Tool for LLVM IR programs to aid Deductive Verification\u201d. MA thesis. University of Twente (2023). http:\/\/essay.utwente.nl\/96536\/"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"van Oorschot, D., Huisman, M., \u015eakar, \u00d6.: First steps towards deductive verification of LLVM IR. In: FASE 2024, LNCS. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-57259-3_15"},{"key":"1_CR42","doi-asserted-by":"publisher","unstructured":"Oortwijn, W., Huisman, M.: Formal verification of an industrial safety-critical traffic tunnel control system. In: Ahrendt, W., Tarifa, S.L.T. (eds.) Integreated Formal Methods (iFM) 2019. LNCS, vol. 11918. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_23","DOI":"10.1007\/978-3-030-34968-4_23"},{"key":"1_CR43","doi-asserted-by":"publisher","unstructured":"Pearce, D.J., Utting, M., Groves, L.: An introduction to software verification with Whiley. In: Bowen, J.P., Liu, Z., Zhang, Z. (eds.) Engineering Trustworthy Software Systems - 4th International School, SETSS 2018, Chongqing, 7\u201312 April 2018, Tutorial Lectures. LNCS, vol. 11430, pp. 1\u201337. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-030-17601-3_1","DOI":"10.1007\/978-3-030-17601-3_1"},{"key":"1_CR44","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. In: ACM Sigplan Notices. PLDI 2013, vol. 48, no. 6, pp. 519\u2013530 (2013). https:\/\/doi.org\/10.1145\/2491956.2462176","DOI":"10.1145\/2491956.2462176"},{"key":"1_CR45","unstructured":"Rijkswaterstaat. Landelijke Tunnelstandaard (National Tunnel Standard). https:\/\/standaarden.rws.nl\/link\/standaard\/6080. Accessed 17 Jan 2024"},{"key":"1_CR46","doi-asserted-by":"publisher","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: European Conference on Object-Oriented Programming (ECOOP). LNCS, vol. 8586. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"1_CR47","unstructured":"Rubbens, R.: Improving Support for Java Exceptions and Inheritance in VerCors. MA thesis. University of Twente (2020). http:\/\/essay.utwente.nl\/81338\/"},{"key":"1_CR48","doi-asserted-by":"publisher","unstructured":"Rubbens, R., Lathouwers, S., Huisman, M.: Modular transformation of Java exceptions modulo errors. In: Lluch-Lafuente, A., Mavridou, A. (eds.) Formal Methods for Industrial Critical Systems - 26th International Conference, FMICS 2021, Paris, 24\u201326 August 2021, Proceedings. LNCS, Vol. 12863, pp. 67\u201384. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_5","DOI":"10.1007\/978-3-030-85248-1_5"},{"key":"1_CR49","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/J.TCS.2022.02.027","volume":"912","author":"M Safari","year":"2022","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","journal-title":"Theor. Comput. Sci."},{"key":"1_CR50","doi-asserted-by":"publisher","unstructured":"Safari, M., Huisman, M.: Formal verification of parallel stream compaction and summed-area table algorithms. In: Pun, V.K.I., Stolz, V., Simao, A. (eds.) Theoretical Aspects of Computing \u2013 ICTAC 2020, pp. 181\u2013199. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-64276-1_10","DOI":"10.1007\/978-3-030-64276-1_10"},{"key":"1_CR51","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., Giannakopoulou, D. (eds.) NASA Formal Methods Symposium, pp. 170\u2013186. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_10","DOI":"10.1007\/978-3-030-55754-6_10"},{"key":"1_CR52","doi-asserted-by":"publisher","unstructured":"\u015eakar, \u00d6., Safari, M., Huisman, M., Wijs, A.: Alpinist: an annotation-aware GPU program optimizer. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022. LNCS, Vol. 13244, pp. 332\u2013352. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_18","DOI":"10.1007\/978-3-030-99527-0_18"},{"key":"1_CR53","doi-asserted-by":"publisher","unstructured":"Schwerhoff, M., Summers, A.J.: Lightweight support for magic wands in an automatic verifier. In: Boyland, J.T. (ed.) 29th European Conference on Object-Oriented Programming, ECOOP 2015, 5\u201310 July 2015, Prague. LIPIcs, vol. 37, pp. 614\u2013638. Schloss Dagstuhl - Leibniz-Zentrum fur Informatik (2015). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2015.614","DOI":"10.4230\/LIPICS.ECOOP.2015.614"},{"key":"1_CR54","unstructured":"Sessink, J.: Verified version of Java\u2019s ArrayList (2022). https:\/\/github.com\/utwente-fmt\/vercors\/tree\/5e3eb17\/examples\/concepts\/arrays\/ArrayList.java. Accessed 17 Jan 2024"},{"key":"1_CR55","doi-asserted-by":"publisher","unstructured":"Sitaraman, M., Weide, B.W.: A synopsis of twenty five years of RESOLVE PhD research efforts: software development effort estimation using ensemble techniques. ACM SIGSOFT Softw. Eng. Notes 43(3), 17 (2018). https:\/\/doi.org\/10.1145\/3229783.3229794","DOI":"10.1145\/3229783.3229794"},{"key":"1_CR56","doi-asserted-by":"publisher","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972). https:\/\/doi.org\/10.1137\/0201010","DOI":"10.1137\/0201010"},{"key":"1_CR57","doi-asserted-by":"publisher","unstructured":"Tasche, P., Monti, R.E., Drerup, S.E., Blohm, P., Herber, P., Huisman, M.: Deductive verification of parameterized embedded systems modeled in SystemC. In: Dimitrova, R., Lahav, O., Wolff, S. (eds.)25th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2024). LNCS, vol. 14500. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-50521-8_9","DOI":"10.1007\/978-3-031-50521-8_9"},{"key":"1_CR58","unstructured":"The Khronos SYCLWorking Group. SYCLTM 2020 Specification (revision 8). Specification. The Khronos Group (2023). https:\/\/registry.khronos.org\/SYCL\/specs\/sycl-2020\/pdf\/sycl-2020.pdf"},{"key":"1_CR59","unstructured":"The OpenCL 1.2 Specification. Khronos Group (2011)"},{"key":"1_CR60","unstructured":"Wittingen, E.: Deductive verification for SYCL. MA thesis. University of Twente (2023). https:\/\/purl.utwente.nl\/essays\/97976"},{"key":"1_CR61","doi-asserted-by":"publisher","unstructured":"Wolf, F.A., Arquint, L., Clochard, M., Oortwijn, W., Pereira, J.C., Muller, P.: Gobra: modular specification and verification of Go programs. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification. LNCS, vol. 12759, pp. 367\u2013379. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_17. ISBN: 978-3-030-81685-8","DOI":"10.1007\/978-3-030-81685-8_17"}],"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-031-65630-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:02:08Z","timestamp":1721858528000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65630-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656293","9783031656309"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65630-9_1","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":"25 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}