{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:02:18Z","timestamp":1781193738915,"version":"3.54.1"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","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-28079-4_20","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:32:48Z","timestamp":1781191968000},"page":"436-455","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Formal Semantics of\u00a0C with\u00a0OpenMP Parallelism"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-2465-1082","authenticated-orcid":false,"given":"Ke","family":"Du","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8686-5835","authenticated-orcid":false,"given":"Anshu","family":"Sharma","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-0244","authenticated-orcid":false,"given":"Liyi","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5351-895X","authenticated-orcid":false,"given":"William","family":"Mansky","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Ahmmed, J., Mahmud, Q.I., Shim, J., Li, L., Jannesari, A., Cohen, M.B.: Differential testing for sequential to parallel transformations. In: Proceedings of the 9th International Workshop on Software Correctness for HPC Applications. Correctness \u201925 (2025)","DOI":"10.1145\/3731599.3767365"},{"key":"20_CR2","unstructured":"Appel, A.W., et al.: Program Logics for Certified Compilers. Cambridge University Press (2014). http:\/\/www.cambridge.org\/de\/academic\/subjects\/computer-science\/programming-languages-and-applied-logic\/program-logics-certified-compilers?format=HB"},{"key":"20_CR3","doi-asserted-by":"publisher","unstructured":"Atzeni, S., Gopalakrishnan, G.: An operational semantic basis for building an OpenMP data race checker. In: 2018 IEEE International Parallel and Distributed Processing Symposium Workshops (IPDPSW), pp. 395\u2013404 (2018). https:\/\/doi.org\/10.1109\/IPDPSW.2018.00074","DOI":"10.1109\/IPDPSW.2018.00074"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-319-22102-1_5","volume-title":"Interactive Theorem Proving","author":"F Besson","year":"2015","unstructured":"Besson, F., Blazy, S., Wilke, P.: A Concrete Memory Model for CompCert. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 67\u201383. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_5"},{"key":"20_CR5","unstructured":"Board, O.A.R.: OpenMP Application Programming Interface (2024). https:\/\/www.openmp.org\/wp-content\/uploads\/OpenMP-API-Specification-6-0.pdf"},{"key":"20_CR6","volume-title":"Compiler correctness for concurrency: from concurrent separation logic to shared-memory assembly language","author":"S Cuellar","year":"2020","unstructured":"Cuellar, S., Giannarakis, N., Madiot, J.M., Mansky, W., Beringer, L., Cao, Q., Appel, A.: Compiler correctness for concurrency: from concurrent separation logic to shared-memory assembly language. Princeton University, Tech. rep. (2020)"},{"key":"20_CR7","doi-asserted-by":"publisher","unstructured":"Ellison, C., Rosu, G.: An Executable Formal Semantics of C with Applications. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 533\u2013544. POPL \u201912, ACM, New York, NY, USA (2012). https:\/\/doi.org\/10.1145\/2103656.2103719","DOI":"10.1145\/2103656.2103719"},{"key":"20_CR8","doi-asserted-by":"publisher","unstructured":"Jiang, H., Liang, H., Xiao, S., Zha, J., Feng, X.: Towards certified separate compilation for concurrent programs. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 111\u2013125. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3314221.3314595","DOI":"10.1145\/3314221.3314595"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10\/c9sb7q, http:\/\/doi.acm.org\/10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Mahmud, Q.I., TehraniJamsaz, A., Ahmed, N.K., Willke, T.L., Jannesari, A.: Contraph: Contrastive learning for parallelization and performance optimization. In: Proceedings of the 39th ACM International Conference on Supercomputing, pp. 596\u2013610 (2025)","DOI":"10.1145\/3721145.3725758"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Mahmud, Q.I., et al.: Autoparllm: GNN-guided context generation for zero-shot code parallelization using LLMs. In: Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies (Vol. 1: Long Papers), pp. 11821\u201311841 (2025)","DOI":"10.18653\/v1\/2025.naacl-long.593"},{"key":"20_CR12","unstructured":"Mattson, T.: A \u201chands-on\u201d introduction to openMP* (2013). https:\/\/www.openmp.org\/wp-content\/uploads\/Intro_To_OpenMP_Mattson.pdf, https:\/\/www.openmp.org\/resources\/tutorials-articles\/"},{"key":"20_CR13","doi-asserted-by":"publisher","unstructured":"Memarian, K., et al.: Exploring C Semantics and Pointer Provenance. Proc. ACM Program. Lang. 3(POPL), 67:1\u201367:32 (2019). https:\/\/doi.org\/10.1145\/3290380","DOI":"10.1145\/3290380"},{"key":"20_CR14","doi-asserted-by":"publisher","unstructured":"Memarian, K., et al.: Into the depths of C: elaborating the de Facto standards. SIGPLAN Not. 51(6), 1\u201315 (2016). https:\/\/doi.org\/10.1145\/2980983.2908081","DOI":"10.1145\/2980983.2908081"},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Siegel, S.F., et al.: Civl: the concurrency intermediate verification language. In: SC \u201915: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, pp. 1\u201312 (2015). https:\/\/doi.org\/10.1145\/2807591.2807635","DOI":"10.1145\/2807591.2807635"},{"key":"20_CR16","first-page":"100965","volume":"37","author":"A Tehrani","year":"2024","unstructured":"Tehrani, A., Bhattacharjee, A., Chen, L., Ahmed, N.K., Yazdanbakhsh, A., Jannesari, A.: Coderosetta: Pushing the boundaries of unsupervised code translation for parallel programming. Adv. Neural. Inf. Process. Syst. 37, 100965\u2013100999 (2024)","journal-title":"Adv. Neural. Inf. Process. Syst."},{"key":"20_CR17","doi-asserted-by":"publisher","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Zappa\u00a0Nardelli, F., Jagannathan, S., Sewell, P.: CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM 60(3), 22:1\u201322:50 (2013). https:\/\/doi.org\/10.1145\/2487241.2487248","DOI":"10.1145\/2487241.2487248"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28079-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:32:52Z","timestamp":1781191972000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_20","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":"12 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}