{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T20:45:05Z","timestamp":1769719505153,"version":"3.49.0"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031787492","type":"print"},{"value":"9783031787508","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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-78750-8_5","type":"book-chapter","created":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T12:15:41Z","timestamp":1739276141000},"page":"93-116","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalisation of\u00a0a\u00a0New Weak Semantics for\u00a0AuDaLa"],"prefix":"10.1007","author":[{"given":"Gijs P.","family":"Leemrijse","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1168-5450","authenticated-orcid":false,"given":"Tom T. P.","family":"Franken","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6117-9129","authenticated-orcid":false,"given":"Thomas","family":"Neele","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,2,12]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Adve, S.V., Hill, M.D.: Weak ordering\u2014a new definition. ACM SIGARCH Comput. Archit. News 18(2SI), 2\u201314 (1990). https:\/\/doi.org\/10.1145\/325096.325100","DOI":"10.1145\/325096.325100"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Aguzzi, G., Casadei, R., Viroli, M.: MacroSwarm: a field-based compositional framework for swarm programming. In: Coordination Models and Languages, pp. 31\u201351. Springer, Switzerland (2023). https:\/\/doi.org\/10.1007\/978-3-031-35361-1_2","DOI":"10.1007\/978-3-031-35361-1_2"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013, vol.\u00a08044, pp. 141\u2013157. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_9","DOI":"10.1007\/978-3-642-39799-8_9"},{"issue":"2","key":"5_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 1\u201374 (2014). https:\/\/doi.org\/10.1145\/2627752. publisher: ACM","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Baba, T., Yoshinaga, T.: A-NETL: a language for massively parallel object-oriented computing. In: PMMPC 1995, pp. 98\u2013105. IEEE (1995). https:\/\/doi.org\/10.1109\/PMMPC.1995.504346","DOI":"10.1109\/PMMPC.1995.504346"},{"key":"5_CR6","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"issue":"1","key":"5_CR7","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0167-6423(90)90044-E","volume":"15","author":"JP Ban\u00e2tre","year":"1990","unstructured":"Ban\u00e2tre, J.P., M\u00e9tayer, D.L.: The gamma model and its discipline of programming. Sci. Comput. Program. 15(1), 55\u201377 (1990). https:\/\/doi.org\/10.1016\/0167-6423(90)90044-E","journal-title":"Sci. Comput. Program."},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Batty, M., Dodds, M., Gotsman, A.: library abstraction for C\/C++ concurrency. In: POPL 2013, January 2013, pp. 235\u2013248. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429099","DOI":"10.1145\/2429069.2429099"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol.\u00a09032, pp. 283\u2013307. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_12","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Batty, M., Memarian, K., Owens, S., Sarkar, S., Sewell, P.: Clarifying and compiling C\/C++ concurrency: from C++11 to POWER. In: POPL 2012, January 2012, pp. 509\u2013520. ACM (2012). https:\/\/doi.org\/10.1145\/2103656.2103717","DOI":"10.1145\/2103656.2103717"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. In: POPL 2011, January 2011, pp. 55\u201366. ACM (2011). https:\/\/doi.org\/10.1145\/1926385.1926394","DOI":"10.1145\/1926385.1926394"},{"issue":"1","key":"5_CR12","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90185-I","volume":"96","author":"G Berry","year":"1992","unstructured":"Berry, G., Boudol, G.: The chemical abstract machine. Theoret. Comput. Sci. 96(1), 217\u2013248 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90185-I","journal-title":"Theoret. Comput. Sci."},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Boehm, H.J., Adve, S.V.: Foundations of the C++ concurrency memory model. In: PLDI 2008, June 2008, pp. 68\u201378. ACM (2008). https:\/\/doi.org\/10.1145\/1375581.1375591","DOI":"10.1145\/1375581.1375591"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Boehm, H.J., Demsky, B.: Outlawing ghosts: avoiding out-of-thin-air results. In: MSPC 2014, pp. 7:1\u20137:6. ACM (2014). https:\/\/doi.org\/10.1145\/2618128.2618134","DOI":"10.1145\/2618128.2618134"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Cagnard, P.J.: The ParCeL-2 programming language. In: Bode, A., Ludwig, T., Karl, W., Wism\u00fcller, R. (eds.) Euro-Par 2000 Parallel Processing. LNCS, vol.\u00a01900, pp. 767\u2013770. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44520-X_106","DOI":"10.1007\/3-540-44520-X_106"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Cenciarelli, P., Knapp, A., Sibilio, E.: The Java memory model: operationally, denotationally, axiomatically. In: De\u00a0Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 331\u2013346. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_23","DOI":"10.1007\/978-3-540-71316-6_23"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Cho, M., Lee, S.H., Hur, C.K., Lahav, O.: Modular data-race-freedom guarantees in the promising semantics. In: PLDI 2021, Virtual, Canada, pp. 867\u2013882. ACM (2021). https:\/\/doi.org\/10.1145\/3453483.3454082","DOI":"10.1145\/3453483.3454082"},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Ciccozzi, F., Addazi, L., Asadollah, S.A., Lisper, B., Masud, A.N., Mubeen, S.: A comprehensive exploration of languages for parallel computing. ACM Comput. Surv. 55(2), 24:1\u201324:39 (2022). https:\/\/doi.org\/10.1145\/3485008","DOI":"10.1145\/3485008"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340 (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Franken, T.T.P., Neele, T., Groote, J.F.: An autonomous data language. In: ICTAC 2023. LNCS, vol. 14446, pp. 158\u2013177. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-47963-2_11","DOI":"10.1007\/978-3-031-47963-2_11"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Gannouni, S.: A Gamma-calculus GPU-based parallel programming framework. In: WSWAN 2015, pp.\u00a01\u20134. IEEE (2015). https:\/\/doi.org\/10.1109\/WSWAN.2015.7210299","DOI":"10.1109\/WSWAN.2015.7210299"},{"issue":"5","key":"5_CR22","first-page":"934","volume":"15","author":"S Gannouni","year":"2018","unstructured":"Gannouni, S., Touir, A., Mathkour, H.: Paradigma: a distributed framework for parallel programming. Int. Arab J. Inf. Technol. 15(5), 934\u2013943 (2018)","journal-title":"Int. Arab J. Inf. Technol."},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Gharachorloo, K., Gupta, A., Hennessy, J.: Performance evaluation of memory consistency models for shared-memory multiprocessors. In: ASPLOS 1991, April 1991, pp. 245\u2013257. ACM (1991). https:\/\/doi.org\/10.1145\/106972.106997","DOI":"10.1145\/106972.106997"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Goens, A., Chakraborty, S., Sarkar, S., Agarwal, S., Oswald, N., Nagarajan, V.: Compound memory models. In: Proceedings of the ACM on Programming Languages, PLDI 2023, June 2023, vol.\u00a07, pp. 1145\u20131168. ACM (2023). https:\/\/doi.org\/10.1145\/3591267","DOI":"10.1145\/3591267"},{"key":"5_CR25","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: Java(TM) Language Specification, 3rd edn. Addison-Wesley Professional (2005)"},{"issue":"1","key":"5_CR26","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1109\/TPDS.2010.62","volume":"22","author":"TD Han","year":"2011","unstructured":"Han, T.D., Abdelrahman, T.: hiCUDA: high-level GPGPU programming. IEEE Trans. Parallel Distrib. Syst. 22(1), 78\u201390 (2011). https:\/\/doi.org\/10.1109\/TPDS.2010.62","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"5_CR27","unstructured":"ISO\/IEC: Programming Languages\u2014C++. International Organization for Standardization, sixth edition edn. (2020). https:\/\/isocpp.org\/files\/papers\/N4860.pdf"},{"issue":"9","key":"5_CR28","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/3338843","volume":"62","author":"D Jackson","year":"2019","unstructured":"Jackson, D.: Alloy: a language and tool for exploring software designs. Commun. ACM 62(9), 66\u201376 (2019). https:\/\/doi.org\/10.1145\/3338843","journal-title":"Commun. ACM"},{"key":"5_CR29","doi-asserted-by":"publisher","unstructured":"Jagadeesan, R., Jeffrey, A., Riely, J.: Pomsets with preconditions: a simple model of relaxed memory. In: Proceedings of the ACM on Programming Languages, OOPSLA 2020, November 2020, vol.\u00a04, pp. 194:1\u2013194:30. ACM (2020). https:\/\/doi.org\/10.1145\/3428262","DOI":"10.1145\/3428262"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Jeffrey, A., Riely, J., Batty, M., Cooksey, S., Kaysin, I., Podkopaev, A.: The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency. In: Proceedings of the ACM on Programming Languages, POPL 2022, January 2022, vol.\u00a06, pp. 54:1\u201354:30. ACM (2022). https:\/\/doi.org\/10.1145\/3498716","DOI":"10.1145\/3498716"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Kang, J., Hur, C.K., Lahav, O., Vafeiadis, V., Dreyer, D.: A promising semantics for relaxed-memory concurrency. In: POPL 2017, January 2017, pp. 175\u2013189. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009850","DOI":"10.1145\/3009837.3009850"},{"key":"5_CR32","unstructured":"Kavanagh, R., Brookes, S.D.: A denotational account of C11-style memory. arXiv arXiv:1804.04214 (2018)"},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C.K., Dreyer, D.: Repairing sequential consistency in C\/C++ 11. In: PLDI 2017, pp. 618\u2013632. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"5_CR34","doi-asserted-by":"publisher","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C-28(9), 690\u2013691 (1979). https:\/\/doi.org\/10.1109\/TC.1979.1675439","DOI":"10.1109\/TC.1979.1675439"},{"key":"5_CR35","doi-asserted-by":"publisher","unstructured":"Lee, S.H., et al.: Promising 2.0: global optimizations in relaxed memory concurrency. In: PLDI 2020, pp. 362\u2013376. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3386010","DOI":"10.1145\/3385412.3386010"},{"key":"5_CR36","unstructured":"Leemrijse, G.P.: The AuDaLaC compiler. GitHub repository (2023). https:\/\/github.com\/GPLeemrijse\/AuDaLaC"},{"key":"5_CR37","doi-asserted-by":"publisher","unstructured":"Leemrijse, G.P.: Towards relaxed memory semantics for the Autonomous Data Language [Supplemental Alloy Files], August 2023. https:\/\/doi.org\/10.5281\/zenodo.8244711","DOI":"10.5281\/zenodo.8244711"},{"key":"5_CR38","doi-asserted-by":"publisher","unstructured":"Leemrijse, G.P., Franken, T.T.P., Neele, T.: Artifact - formalisation of a new weak semantics for AuDaLa, August 2024. https:\/\/doi.org\/10.5281\/zenodo.13358993","DOI":"10.5281\/zenodo.13358993"},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Leiserson, C.E., et al.: There\u2019s plenty of room at the top: what will drive computer performance after Moore\u2019s law? Science 368(6495), eaam9744 (2020). https:\/\/doi.org\/10.1126\/science.aam9744","DOI":"10.1126\/science.aam9744"},{"key":"5_CR40","doi-asserted-by":"publisher","unstructured":"Liu, L., Millstein, T., Musuvathi, M.: Accelerating sequential consistency for Java with speculative compilation. In: PLDI 2019, pp. 16\u201330. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314611","DOI":"10.1145\/3314221.3314611"},{"key":"5_CR41","doi-asserted-by":"publisher","unstructured":"Lustig, D., Cooksey, S., Giroux, O.: Mixed-proxy extensions for the NVIDIA PTX memory consistency model: industrial product. In: ISCA 2022, pp. 1058\u20131070. ACM (2022). https:\/\/doi.org\/10.1145\/3470496.3533045","DOI":"10.1145\/3470496.3533045"},{"key":"5_CR42","doi-asserted-by":"publisher","unstructured":"Lustig, D., Sahasrabuddhe, S., Giroux, O.: A formal analysis of the NVIDIA PTX memory consistency model. In: ASPLOS 2019, pp. 257\u2013270. ACM (2019). https:\/\/doi.org\/10.1145\/3297858.3304043","DOI":"10.1145\/3297858.3304043"},{"key":"5_CR43","doi-asserted-by":"publisher","unstructured":"Lustig, D., Wright, A., Papakonstantinou, A., Giroux, O.: Automated synthesis of comprehensive memory model litmus test suites. In: ASPLOS 2017, pp. 661\u2013675. ACM (2017). https:\/\/doi.org\/10.1145\/3037697.3037723","DOI":"10.1145\/3037697.3037723"},{"key":"5_CR44","doi-asserted-by":"publisher","unstructured":"Marino, D., Singh, A., Millstein, T., Musuvathi, M., Narayanasamy, S.: A case for an SC-preserving compiler. In: PLDI 2011, June 2011, pp. 199\u2013210. ACM (2011). https:\/\/doi.org\/10.1145\/1993316.1993522","DOI":"10.1145\/1993316.1993522"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Nagarajan, V., Sorin, D.J., Hill, M.D., Wood, D.A.: A Primer on Memory Consistency and Cache Coherence. Springer, Heidelberg (2020)","DOI":"10.1007\/978-3-031-01764-3"},{"key":"5_CR46","doi-asserted-by":"publisher","unstructured":"Nienhuis, K., Memarian, K., Sewell, P.: An operational semantics for C\/C++11 concurrency. In: OOPSLA 2016, October 2016, pp. 111\u2013128. ACM (2016). https:\/\/doi.org\/10.1145\/2983990.2983997","DOI":"10.1145\/2983990.2983997"},{"key":"5_CR47","unstructured":"NVIDIA: PTX ISA, edition 8.2 (2023). https:\/\/docs.nvidia.com\/cuda\/parallel-thread-execution\/index.html"},{"key":"5_CR48","unstructured":"OpenMP Architecture Review Board: OpenMP Application Program Interface Version 5.0, January 2023. https:\/\/www.openmp.org\/wp-content\/uploads\/OpenMP-API-Specification-5.0.pdf"},{"key":"5_CR49","doi-asserted-by":"publisher","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 391\u2013407. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_27","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"5_CR50","doi-asserted-by":"publisher","unstructured":"Paviotti, M., Cooksey, S., Paradis, A., Wright, D., Owens, S., Batty, M.: Modular relaxed dependencies in weak memory concurrency. In: M\u00fcller, P. (ed.) ESOP 2020. LNCS, vol. 12075, pp. 599\u2013625. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_22","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"5_CR51","doi-asserted-by":"crossref","unstructured":"Rudy, G.: CUDA-CHiLL: a programming language interface for GPGPU optimizations and code generation (2010)","DOI":"10.1007\/978-3-642-19595-2_10"},{"key":"5_CR52","doi-asserted-by":"publisher","unstructured":"Sorensen, T., Donaldson, A.F.: Exposing errors related to weak memory in GPU applications. In: PLDI 2016, June 2016, pp. 100\u2013113. ACM (2016). https:\/\/doi.org\/10.1145\/2908080.2908114","DOI":"10.1145\/2908080.2908114"},{"key":"5_CR53","doi-asserted-by":"publisher","unstructured":"Sozeau, M., et al.: The Coq Proof Assistant, June 2023. https:\/\/doi.org\/10.5281\/zenodo.8161141, version Number: 8.17","DOI":"10.5281\/zenodo.8161141"},{"key":"5_CR54","doi-asserted-by":"publisher","unstructured":"Ueng, S.Z., Lathara, M., Baghsorkhi, S.S., Hwu, W.W.: CUDA-Lite: reducing GPU programming complexity. In: Amaral, J.N. (ed.) LCPC. vol.\u00a05335, pp. 1\u201315. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89740-8_1","DOI":"10.1007\/978-3-540-89740-8_1"},{"key":"5_CR55","doi-asserted-by":"publisher","unstructured":"Ungar, D., Adams, S.S.: Harnessing emergence for manycore programming: early experience integrating ensembles, adverbs, and object-based inheritance. In: OOPSLA 2010, pp. 19\u201326. ACM (2010). https:\/\/doi.org\/10.1145\/1869542.1869546","DOI":"10.1145\/1869542.1869546"},{"key":"5_CR56","doi-asserted-by":"publisher","unstructured":"Vafeiadis, V., Balabonski, T., Chakraborty, S., Morisset, R., Zappa\u00a0Nardelli, F.: Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In: POPL 2015, January 2015, pp. 209\u2013220. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2676995","DOI":"10.1145\/2676726.2676995"},{"key":"5_CR57","doi-asserted-by":"publisher","unstructured":"Vafeiadis, V., Narayan, C.: Relaxed separation logic: a program logic for C11 concurrency. In: OOPSLA 2013, October 2013, pp. 867\u2013884. ACM (2013). https:\/\/doi.org\/10.1145\/2509136.2509532","DOI":"10.1145\/2509136.2509532"},{"key":"5_CR58","doi-asserted-by":"publisher","unstructured":"Vialle, S., Cornu, T., Lallement, Y.: ParCeL-1: a parallel programming language based on autonomous and synchronous actors. SIGPLAN Not. 31(8), 43\u201351 (1996). https:\/\/doi.org\/10.1145\/242903.2429, publisher: ACM","DOI":"10.1145\/242903.2429"},{"key":"5_CR59","doi-asserted-by":"publisher","unstructured":"Watt, C., et al.: Repairing and mechanising the JavaScript relaxed memory model. In: PLDI 2020, pp. 346\u2013361. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385973","DOI":"10.1145\/3385412.3385973"},{"key":"5_CR60","doi-asserted-by":"publisher","unstructured":"Wickerson, J., Batty, M., Sorensen, T., Constantinides, G.A.: Automatically comparing memory consistency models. In: POPL 2017, pp. 190\u2013204. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009838","DOI":"10.1145\/3009837.3009838"},{"issue":"6","key":"5_CR61","doi-asserted-by":"publisher","first-page":"1647","DOI":"10.1109\/TPDS.2015.2453978","volume":"27","author":"J Yan","year":"2016","unstructured":"Yan, J., Tan, G., Mo, Z., Sun, N.: Graphine: programming graph-parallel computation of large natural graphs for multicore clusters. IEEE Trans. Parallel Distrib. Syst. 27(6), 1647\u20131659 (2016). https:\/\/doi.org\/10.1109\/TPDS.2015.2453978","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"12","key":"5_CR62","doi-asserted-by":"publisher","first-page":"1270","DOI":"10.14778\/2536274.2536293","volume":"6","author":"J Zhong","year":"2013","unstructured":"Zhong, J., He, B.: Parallel graph processing on graphics processors made easy. Proc. VLDB Endow. 6(12), 1270\u20131273 (2013). https:\/\/doi.org\/10.14778\/2536274.2536293","journal-title":"Proc. VLDB Endow."},{"key":"5_CR63","doi-asserted-by":"publisher","unstructured":"\u0160ev\u010d\u00edk, J.: Safe optimisations for shared-memory concurrent programs. In: PLDI 2011, June 2011, pp. 306\u2013316. ACM (2011). https:\/\/doi.org\/10.1145\/1993498.1993534","DOI":"10.1145\/1993498.1993534"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-78750-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T10:08:32Z","timestamp":1769681312000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-78750-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031787492","9783031787508"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-78750-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"12 February 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","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":"21 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}