{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T08:44:07Z","timestamp":1777106647823,"version":"3.51.4"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,3,5]],"date-time":"2021-03-05T00:00:00Z","timestamp":1614902400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,3,5]],"date-time":"2021-03-05T00:00:00Z","timestamp":1614902400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1138996"],"award-info":[{"award-number":["CCF-1138996"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["XPS-1337174"],"award-info":[{"award-number":["XPS-1337174"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,2]]},"DOI":"10.1007\/s10703-021-00362-8","type":"journal-article","created":{"date-parts":[[2021,3,5]],"date-time":"2021-03-05T11:02:56Z","timestamp":1614942176000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Static detection of uncoalesced accesses in GPU programs"],"prefix":"10.1007","volume":"60","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joseph","family":"Devietti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Omar S. Navarro","family":"Leija","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1345-0505","authenticated-orcid":false,"given":"Nimit","family":"Singhania","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,5]]},"reference":[{"key":"362_CR1","doi-asserted-by":"publisher","unstructured":"Allen JR, Kennedy K, Porterfield C, Warren J (1983) Conversion of control dependence to data dependence. In: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on principles of programming languages, POPL \u201983. ACM, New York, NY, USA, pp 177\u2013189. https:\/\/doi.org\/10.1145\/567067.567085","DOI":"10.1145\/567067.567085"},{"key":"362_CR2","doi-asserted-by":"publisher","unstructured":"Amilkanthwar M, Balachandran, S (2013) CUPL: A compile-time uncoalesced memory access pattern locator for CUDA. In: Proceedings of the 27th international ACM conference on international conference on supercomputing, ICS \u201913. ACM, New York, NY, USA, pp 459\u2013460. https:\/\/doi.org\/10.1145\/2464996.2467288","DOI":"10.1145\/2464996.2467288"},{"key":"362_CR3","doi-asserted-by":"publisher","unstructured":"Baskaran MM, Bondhugula U, Krishnamoorthy S, Ramanujam J, Rountev A, Sadayappan P (2008) A compiler framework for optimization of affine loop nests for GPGPUs. In: Proceedings of the 22Nd annual international conference on supercomputing, ICS \u201908. ACM, New York, NY, USA, pp 225\u2013234. https:\/\/doi.org\/10.1145\/1375527.1375562","DOI":"10.1145\/1375527.1375562"},{"issue":"10","key":"362_CR4","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/2398857.2384625","volume":"47","author":"A Betts","year":"2012","unstructured":"Betts A, Chong N, Donaldson A, Qadeer S, Thomson P (2012) GPUVerify: a verifier for GPU kernels. SIGPLAN Notice 47(10):113\u2013132. https:\/\/doi.org\/10.1145\/2398857.2384625","journal-title":"SIGPLAN Notice"},{"issue":"3","key":"362_CR5","doi-asserted-by":"publisher","first-page":"10:1","DOI":"10.1145\/2743017","volume":"37","author":"A Betts","year":"2015","unstructured":"Betts A, Chong N, Donaldson AF, Ketema J, Qadeer S, Thomson P, Wickerson J (2015) The design and implementation of a verification technique for GPU kernels. ACM Trans Program Lang Syst 37(3):10:1-10:49. https:\/\/doi.org\/10.1145\/2743017","journal-title":"ACM Trans Program Lang Syst"},{"key":"362_CR6","doi-asserted-by":"publisher","unstructured":"Boyer RS, Elspas B, Levitt KN (1975) SELECT \u2013 a formal system for testing and debugging programs by symbolic execution. In: Proceedings of the international conference on reliable software. ACM, New York, NY, USA, pp 234\u2013245. https:\/\/doi.org\/10.1145\/800027.808445","DOI":"10.1145\/800027.808445"},{"key":"362_CR7","doi-asserted-by":"publisher","unstructured":"Che S, Boyer M, Meng J, Tarjan D, Sheaffer JW, Lee SH, Skadron K (2009) Rodinia: A benchmark suite for heterogeneous computing. In: Proceedings of the 2009 IEEE international symposium on workload characterization (IISWC), IISWC \u201909. IEEE Computer Society, Washington, DC, USA, pp 44\u201354. https:\/\/doi.org\/10.1109\/IISWC.2009.5306797","DOI":"10.1109\/IISWC.2009.5306797"},{"key":"362_CR8","doi-asserted-by":"publisher","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on principles of programming languages, POPL \u201977. ACM, New York, NY, USA, pp 238\u2013252. https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"362_CR9","doi-asserted-by":"crossref","unstructured":"Fauzia N, Pouchet LN, Sadayappan P (2015) Characterizing and enhancing global memory data coalescing on GPUs. In: Proceedings of the 13th Annual IEEE\/ACM international symposium on code generation and optimization, CGO \u201915. IEEE Computer Society, Washington, DC, USA, pp 12\u201322. http:\/\/dl.acm.org\/citation.cfm?id=2738600.2738603","DOI":"10.1109\/CGO.2015.7054183"},{"key":"362_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-658-10113-8","volume-title":"Automatic SIMD Vectorization of SSA-based Control Flow Graphs","author":"R Karrenberg","year":"2015","unstructured":"Karrenberg R (2015) Automatic SIMD Vectorization of SSA-based Control Flow Graphs. Springer, Berlin"},{"key":"362_CR11","doi-asserted-by":"publisher","unstructured":"Kim Y, Shrivastava A (2011) CuMAPz: A tool to analyze memory access patterns in CUDA. In: Proceedings of the 48th design automation conference, DAC \u201911. ACM, New York, NY, USA, pp 128\u2013133. https:\/\/doi.org\/10.1145\/2024724.2024754","DOI":"10.1145\/2024724.2024754"},{"key":"362_CR12","doi-asserted-by":"publisher","unstructured":"King JC (1975) A new approach to program testing. In: Proceedings of the International Conference on Reliable Software. ACM, New York, NY, USA, pp 228\u2013233. https:\/\/doi.org\/10.1145\/800027.808444","DOI":"10.1145\/800027.808444"},{"key":"362_CR13","doi-asserted-by":"publisher","unstructured":"Li G, Gopalakrishnan G (2010) Scalable SMT-based verification of GPU kernel functions. In: Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE \u201910. ACM, New York, NY, USA, pp 187\u2013196. https:\/\/doi.org\/10.1145\/1882291.1882320","DOI":"10.1145\/1882291.1882320"},{"key":"362_CR14","doi-asserted-by":"publisher","unstructured":"Li G, Li P, Sawaya G, Gopalakrishnan G, Ghosh I, Rajan SP (2012) GKLEE: Concolic verification and test generation for GPUs. In: Proceedings of the 17th ACM SIGPLAN symposium on principles and practice of parallel programming, PPoPP \u201912. ACM, New York, NY, USA, pp 215\u2013224. https:\/\/doi.org\/10.1145\/2145816.2145844","DOI":"10.1145\/2145816.2145844"},{"key":"362_CR15","doi-asserted-by":"publisher","unstructured":"Moll S, Hack S (2018) Partial control-flow linearization. In: Proceedings of the 39th ACM SIGPLAN conference on programming language design and implementation, PLDI 2018. ACM, New York, NY, USA, pp 543\u2013556. https:\/\/doi.org\/10.1145\/3192366.3192413","DOI":"10.1145\/3192366.3192413"},{"key":"362_CR16","volume-title":"Principles of program analysis","author":"F Nielson","year":"2010","unstructured":"Nielson F, Nielson HR, Hankin C (2010) Principles of program analysis. Springer, Cham"},{"key":"362_CR17","unstructured":"Nvidia: CUDA C Programming Guide v9.0. http:\/\/docs.nvidia.com\/cuda\/cuda-c-programming-guide\/"},{"key":"362_CR18","unstructured":"Nvidia: Nvidia Performance Analysis Tools. http:\/\/developer.nvidia.com\/performance-analysis-tools\/"},{"key":"362_CR19","doi-asserted-by":"publisher","unstructured":"Pharr M, Mark WR (2012) ispc: A spmd compiler for high-performance cpu programming. In: 2012 innovative parallel computing (InPar), pp 1\u201313. https:\/\/doi.org\/10.1109\/InPar.2012.6339601","DOI":"10.1109\/InPar.2012.6339601"},{"key":"362_CR20","doi-asserted-by":"publisher","unstructured":"Sung IJ, Stratton JA, Hwu WMW (2010) Data layout transformation exploiting memory-level parallelism in structured grid many-core applications. In: Proceedings of the 19th international conference on parallel architectures and compilation techniques, PACT \u201910. ACM, New York, NY, USA, pp 513\u2013522. https:\/\/doi.org\/10.1145\/1854273.1854336","DOI":"10.1145\/1854273.1854336"},{"key":"362_CR21","doi-asserted-by":"publisher","unstructured":"Ueng SZ, Lathara M, Baghsorkhi SS, Hwu WMW (2008) Languages and compilers for parallel computing. chap. CUDA-Lite: reducing GPU Programming Complexity. Springer, Berlin, pp 1\u201315. https:\/\/doi.org\/10.1007\/978-3-540-89740-8_1","DOI":"10.1007\/978-3-540-89740-8_1"},{"key":"362_CR22","doi-asserted-by":"publisher","unstructured":"Wu J, Belevich A, Bendersky E, Heffernan M, Leary C, Pienaar J, Roune B, Springer R, Weng X, Hundt R (2016) Gpucc: An open-source GPGPU compiler. In: Proceedings of the 2016 international symposium on code generation and optimization, CGO \u201916. ACM, New York, NY, USA, pp 105\u2013116. https:\/\/doi.org\/10.1145\/2854038.2854041","DOI":"10.1145\/2854038.2854041"},{"key":"362_CR23","doi-asserted-by":"publisher","unstructured":"Yang Y, Xiang P, Kong J, Zhou H (2010) A GPGPU compiler for memory optimization and parallelism management. In: Proceedings of the 31st ACM SIGPLAN conference on programming language design and implementation, PLDI \u201910. ACM, New York, NY, USA, pp 86\u201397. https:\/\/doi.org\/10.1145\/1806596.1806606","DOI":"10.1145\/1806596.1806606"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00362-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00362-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00362-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T17:30:09Z","timestamp":1675877409000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00362-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,5]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["362"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00362-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,3,5]]},"assertion":[{"value":"18 November 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 February 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 March 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}