{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:56:18Z","timestamp":1782867378975,"version":"3.54.5"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-22749-2_13","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:13:33Z","timestamp":1776258813000},"page":"257-276","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["jMT: Testing Correctness of Java Memory Models"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9241-5583","authenticated-orcid":false,"given":"Lukas","family":"Panneke","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2385-7512","authenticated-orcid":false,"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","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), 7:1\u20137:74 (2014). https:\/\/doi.org\/10.1145\/2627752","DOI":"10.1145\/2627752"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Aspinall, D., \u0160ev\u010d\u00edk, J.: Formalising Java\u2019s data race free guarantee. In: Schneider, K., Brandt, J. (eds.) TPHOL\u201907. pp. 22\u201337. LNCS 4732, Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-74591-4_4","DOI":"10.1007\/978-3-540-74591-4_4"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: ESOP. Lecture Notes in Computer Science, vol.\u00a09032, pp. 283\u2013307. Springer (2015)","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Bender, J., Palsberg, J.: A formalization of Java\u2019s concurrent access modes. Proc. ACM Program. Lang. 3(OOPSLA), 142:1\u2013142:28 (2019)","DOI":"10.1145\/3360568"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Cenciarelli, P., Knapp, A., Sibilio, E.: The Java memory model: Operationally, denotationally, axiomatically. In: ESOP. Lecture Notes in Computer Science, vol.\u00a04421, pp. 331\u2013346. Springer (2007)","DOI":"10.1007\/978-3-540-71316-6_23"},{"key":"13_CR6","doi-asserted-by":"publisher","unstructured":"Gavrilenko, N., de\u00a0Le\u00f3n, H.P., Furbach, F., Heljanko, K., Meyer, R.: BMC for weak memory models: Relation analysis for compact SMT encodings. In: Dillig, I., Tasiran, S. (eds.) CAV\u201919\u2019. pp. 355\u2013365. LNCS 11561, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_19","DOI":"10.1007\/978-3-030-25540-4_19"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Geeson, L., Smith, L.: Compiler testing with relaxed memory models. In: CGO. pp. 334\u2013348. IEEE (2024)","DOI":"10.1109\/CGO57630.2024.10444836"},{"key":"13_CR8","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java language specification (1996)"},{"key":"13_CR9","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G., Buckley, A., Smith, D., Bierman, G.: Java language specification - Chapter 17. threads and locks - 17.4. memory model, https:\/\/docs.oracle.com\/javase\/specs\/jls\/se24\/html\/jls-17.html#jls-17.4"},{"key":"13_CR10","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. Proc. ACM Program. Lang. 6(POPL), 1\u201330 (2022). https:\/\/doi.org\/10.1145\/3498716","DOI":"10.1145\/3498716"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Jorshari, M.H.K., Kokologiannakis, M., Majumdar, R., Nagendra, S.: Optimal concolic dynamic partial order reduction. In: Bouyer, P., van\u00a0de Pol, J. (eds.) CONCUR\u201925. LIPIcs, vol.\u00a0348, pp. 26:1\u201326:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2025). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2025.26","DOI":"10.4230\/LIPICS.CONCUR.2025.26"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Kokologiannakis, M., Vafeiadis, V.: Genmc: A model checker for weak memory models. In: Silva, A., Leino, K.R.M. (eds.) CAV\u201921. pp. 427\u2013440. LNCS 12759, Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_20","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"13_CR13","unstructured":"Lahav, O.: A case against semantic dependencies. In: The Future of Weak Memory 2024. https:\/\/popl24.sigplan.org\/details\/fowm-2024-papers\/8\/A-case-against-semantic-dependencies, recording of talk avaliable at https:\/\/youtu.be\/7VZtwIvZ6qE"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Lahav, O., Boker, U.: Decidable verification under a causally consistent shared memory. In: Donaldson, A.F., Torlak, E. (eds.) PLDI\u201920. pp. 211\u2013226. ACM (2020). https:\/\/doi.org\/10.1145\/3385412.3385966","DOI":"10.1145\/3385412.3385966"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Lahav, O., Vafeiadis, V., Kang, J., Hur, C., Dreyer, D.: Repairing sequential consistency in C\/C++11. In: Cohen, A., Vechev, M.T. (eds.) PLDI\u201917. pp. 618\u2013632. ACM (2017). https:\/\/doi.org\/10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"13_CR16","unstructured":"Lea, D.: Using JDK 9 memory order modes, https:\/\/gee.cs.oswego.edu\/dl\/html\/j9mm.html"},{"key":"13_CR17","unstructured":"Liu, S., Bender, J., Palsberg, J.: Compiling volatile correctly in Java. In: ECOOP. LIPIcs, vol.\u00a0222, pp. 6:1\u20136:26. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Liu, S., Bender, J., Palsberg, J.: Compiling volatile correctly in Java. In: Ali, K., Vitek, J. (eds.) ECOOP\u201922. pp. 6:1\u201326. LIPIcs 222, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2022.6","DOI":"10.4230\/LIPICS.ECOOP.2022.6"},{"key":"13_CR19","unstructured":"Manson, J.: Volatile fields and synchronization, https:\/\/jeremymanson.blogspot.com\/2007\/03\/volatile-fields-and-synchronization.html"},{"key":"13_CR20","unstructured":"Manson, J.: The Java Memory Model. Ph.D. thesis, University of Maryland, College Park, MD, USA (2004), https:\/\/hdl.handle.net\/1903\/1949"},{"key":"13_CR21","unstructured":"Manson, J., Pugh, W.: The Java memory model simulator. In: FTfJP\u201902 (2002)"},{"key":"13_CR22","unstructured":"Manson, J., Pugh, W., Adve, S.: The Java memory model https:\/\/web.archive.org\/web\/20060303190317http:\/\/www.cs.umd.edu\/users\/jmanson\/java\/journal.pdf, original URL: http:\/\/www.cs.umd.edu\/users\/jmanson\/java\/journal.pdf, archived 2006-03-03"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W.W., Adve, S.V.: The Java memory model. In: POPL. pp. 378\u2013391. ACM (2005)","DOI":"10.1145\/1040305.1040336"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Moiseenko, E., Kokologiannakis, M., Vafeiadis, V.: Model checking for a multi-execution memory model. Proc. ACM Program. Lang. 6(OOPSLA2), 758\u2013785 (2022). https:\/\/doi.org\/10.1145\/3563315","DOI":"10.1145\/3563315"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Panneke, L., Wehrheim, H.: jMT: Testing correctness of Java memory models (artifact) (Oct 2025). https:\/\/doi.org\/10.5281\/zenodo.17634679","DOI":"10.5281\/zenodo.17634679"},{"key":"13_CR26","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.) ESOP20. pp. 599\u2013625. LNCS 12075, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_22","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Petri, G., Vitek, J., Jagannathan, S.: Cooking the books: Formalizing JMM implementation recipes. In: Boyland, J.T. (ed.) ECOOP\u201915. LIPIcs, vol.\u00a037, pp. 445\u2013469. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2015.445","DOI":"10.4230\/LIPICS.ECOOP.2015.445"},{"key":"13_CR28","unstructured":"Pugh, W.: Causality test cases, https:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/CausalityTestCases.html"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Pugh, W.W.: Fixing the Java memory model. In: Java Grande. pp. 89\u201398. ACM (1999)","DOI":"10.1145\/304065.304106"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Richards, J., Wright, D., Cooksey, S., Batty, M.: Symbolic MRD: Dynamic memory, undefined behaviour, and extrinsic choice. Proc. ACM Program. Lang. 9(OOPSLA1), 1858\u20131882 (2025). https:\/\/doi.org\/10.1145\/3721089","DOI":"10.1145\/3721089"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"\u0160ev\u010d\u00edk, J., Aspinall, D.: On validity of program transformations in the Java memory model. In: Vitek, J. (ed.) ECOOP\u201908. pp. 27\u201351. LNCS 5142, Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-70592-5_3","DOI":"10.1007\/978-3-540-70592-5_3"},{"key":"13_CR32","unstructured":"Shipil\u00ebv, A.: Close encounters of the Java memory model kind, https:\/\/shipilev.net\/blog\/2016\/close-encounters-of-jmm-kind\/"},{"key":"13_CR33","unstructured":"Shipil\u00ebv, A., et\u00a0al.: Java concurrency stress (jcstress) (2013), https:\/\/github.com\/openjdk\/jcstress\/"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"Trippel, C., Manerkar, Y.A., Lustig, D., Pellauer, M., Martonosi, M.: TriCheck: Memory model verification at the trisection of software, hardware, and ISA. In: Chen, Y., Temam, O., Carter, J. (eds.) ASPLOS\u201917. pp. 119\u2013133. ACM (2017). https:\/\/doi.org\/10.1145\/3037697.3037719","DOI":"10.1145\/3037697.3037719"}],"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-032-22749-2_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:17:12Z","timestamp":1782865032000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_13","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":"15 April 2026","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":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","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":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}