{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:39:52Z","timestamp":1780994392340,"version":"3.54.1"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,5,22]],"date-time":"2015-05-22T00:00:00Z","timestamp":1432252800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EPSRC-funded PhD studentships"},{"name":"EPSRC project EP\/G051100\/2"},{"name":"EU FP7 STREP project CARP (project number 287767)"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2015,6,18]]},"abstract":"<jats:p>We present a technique for the formal verification of GPU kernels, addressing two classes of correctness properties: data races and barrier divergence. Our approach is founded on a novel formal operational semantics for GPU kernels termed &lt;i&gt;synchronous, delayed visibility (SDV)&lt;\/i&gt; semantics, which captures the execution of a GPU kernel by multiple groups of threads. The SDV semantics provides operational definitions for barrier divergence and for both inter- and intra-group data races. We build on the semantics to develop a method for reducing the task of verifying a massively parallel GPU kernel to that of verifying a sequential program. This completely avoids the need to reason about thread interleavings, and allows existing techniques for sequential program verification to be leveraged. We describe an efficient encoding of data race detection and propose a method for automatically inferring the loop invariants that are required for verification. We have implemented these techniques as a practical verification tool, GPUVerify, that can be applied directly to OpenCL and CUDA source code. We evaluate GPUVerify with respect to a set of 162 kernels drawn from public and commercial sources. Our evaluation demonstrates that GPUVerify is capable of efficient, automatic verification of a large number of real-world kernels.<\/jats:p>","DOI":"10.1145\/2743017","type":"journal-article","created":{"date-parts":[[2015,5,26]],"date-time":"2015-05-26T14:36:05Z","timestamp":1432650965000},"page":"1-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":53,"title":["The Design and Implementation of a Verification Technique for GPU Kernels"],"prefix":"10.1145","volume":"37","author":[{"given":"Adam","family":"Betts","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nathan","family":"Chong","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeroen","family":"Ketema","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[{"name":"Microsoft Research Redmond, WA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul","family":"Thomson","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Wickerson","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2015,5,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694391"},{"key":"e_1_2_1_2_1","unstructured":"AMD. 2013. OpenCL Programming Guide Revision 2.7. Retrieved from http:\/\/developer.amd.com\/wordpress\/media\/2013\/07\/AMD&lowbar;Accelerated&lowbar;Parallel&lowbar;Processing&lowbar;OpenCL&lowbar;Programming&lowbar;Guide-rev-2.7.pdf."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_15"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 6th NASA Formal Methods Symposium (NFM\u201914)","volume":"8430","author":"Bardsley Ethel","unstructured":"Ethel Bardsley and Alastair F. Donaldson. 2014. Warps and atomics: Beyond barrier synchronization in the verification of GPU kernels. In Proceedings of the 6th NASA Formal Methods Symposium (NFM\u201914). Lecture Notes in Computer Science, Vol. 8430. Springer, Berlin, 230--245."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2664666.2664673"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1646353.1646374"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384625"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250769"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.03.013"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 3rd Workshop on Software Tools for MultiCore Systems (STMCS\u201908)","author":"Boyer Michael","year":"2008","unstructured":"Michael Boyer, Kevin Skadron, and Westley Weimer. 2008. Automated dynamic analysis of CUDA programs. In Proceedings of the 3rd Workshop on Software Tools for MultiCore Systems (STMCS\u201908). Retrieved from http:\/\/people.csail.mit.edu\/rabbah\/conferences\/08\/cgo\/stmcs\/."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855756"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.media.2004.06.022"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_15"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509517"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535882"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34188-5_18"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_16"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_23_1","volume-title":"Article 1","author":"Donaldson Alastair F.","year":"2014","unstructured":"Alastair F. Donaldson. 2014. The GPUVerify method: A tutorial overview. Electronic Communications of the EASST 70, Article 1 (2014), 16 pages. Retrieved from http:\/\/journal.ub.tu-berlin.de\/eceasst\/article\/view\/986."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_24"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0124-2"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926432"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733618"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_16"},{"key":"e_1_2_1_31_1","volume-title":"GPU Gems","author":"Harris Mark J.","unstructured":"Mark J. Harris. 2004. Fast fluid dynamics simulation on the GPU. In GPU Gems. Addison-Wesley, Boston, MA, 637--665."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986326"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1941553.1941573"},{"key":"e_1_2_1_34_1","unstructured":"Khronos OpenCL Working Group. 2012. The OpenCL Specification Version 1.2. Document revision 19. Retrieved from https:\/\/www.khronos.org\/registry\/cl\/specs\/opencl-1.2.pdf."},{"key":"e_1_2_1_35_1","unstructured":"Khronos OpenCL Working Group. 2014a. The OpenCL C Specification Version 2.0. Document revision 26. Retrieved from https:\/\/www.khronos.org\/registry\/cl\/specs\/opencl-2.0-openclc.pdf."},{"key":"e_1_2_1_36_1","unstructured":"Khronos OpenCL Working Group. 2014b. The OpenCL Extension Specification Version 2.0. Document revision 26. Retrieved from https:\/\/www.khronos.org\/registry\/cl\/specs\/opencl-2.0-extensions.pdf."},{"key":"e_1_2_1_37_1","volume-title":"Graham Pullan, Ian McFarlane, Giles S. H. Yeo, and Brian Y. H. Lam.","author":"Klus Petr","year":"2012","unstructured":"Petr Klus, Simon Lam, Dag Lyberg, Ming Sin Cheung, Graham Pullan, Ian McFarlane, Giles S. H. Yeo, and Brian Y. H. Lam. 2012. BarraCUDA\u2014A fast short read sequence aligner using graphics processing units. BMC Research Notes 5, Article 27 (2012), 7 pages."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_5"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_18"},{"key":"e_1_2_1_40_1","volume-title":"Saxe","author":"Leino K. Rustan M.","year":"2000","unstructured":"K. Rustan M. Leino, Greg Nelson, and James B. Saxe. 2000. ESC\/Java User\u2019s Manual. Technical Report SRC Technical Note 2000-002. Compaq Systems Research Center."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254110"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882320"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2145816.2145844"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1093\/bioinformatics\/btp324"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2012.94"},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the 2nd UK GPU Computing Conference.","author":"Lokhmotov Anton","year":"2011","unstructured":"Anton Lokhmotov. 2011. Mobile and Embedded Computing on Mali GPUs. In Proceedings of the 2nd UK GPU Computing Conference."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/646704.702020"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_2_1_49_1","unstructured":"Microsoft Corporation. 2012. C&plus;&plus; AMP: Language and Programming Model Version 1.0. Retrieved from http:\/\/download.microsoft.com\/download\/4\/0\/E\/40EA02D8-23A7-4BD2-AD3A-0BFFFB640F28\/CppAMPLanguageAndProgrammingModel.pdf."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/1791547"},{"key":"e_1_2_1_51_1","unstructured":"Nvidia. 2012a. CUDA C Programming Guide Version 5.0. http:\/\/docs.nvidia.com\/cuda\/cuda-c-programming-guide\/."},{"key":"e_1_2_1_52_1","unstructured":"Nvidia. 2012b. Parallel Thread Execution ISA Version 3.1."},{"key":"e_1_2_1_53_1","unstructured":"Lars Nyland. 2012. Personal Communication."},{"key":"e_1_2_1_54_1","volume-title":"Fast N-Body Simulation with CUDA","author":"Nyland Lars","unstructured":"Lars Nyland, Mark Harris, and Jan Prins. 2007. Fast N-Body Simulation with CUDA. Addison-Wesley, Upper Saddle River, NJ, 677--696."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2013.178"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542501"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517434"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.21236\/ADA538815"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.07.053"},{"key":"e_1_2_1_61_1","unstructured":"John Wickerson. 2014. Syntax and semantics of a GPU kernel programming language. Archive of Formal Proofs. Retrieved from http:\/\/afp.sourceforge.net\/entries\/GPU_Kernel_PL.shtml."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2743017","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2743017","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:34Z","timestamp":1750227394000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2743017"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,22]]},"references-count":61,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,6,18]]}},"alternative-id":["10.1145\/2743017"],"URL":"https:\/\/doi.org\/10.1145\/2743017","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,22]]},"assertion":[{"value":"2014-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-05-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}