{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:44:34Z","timestamp":1770288274588,"version":"3.49.0"},"publisher-location":"New York, New York, USA","reference-count":12,"publisher":"ACM Press","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1145\/2664666.2664673","type":"proceedings-article","created":{"date-parts":[[2015,2,23]],"date-time":"2015-02-23T16:02:15Z","timestamp":1424707335000},"page":"1-5","source":"Crossref","is-referenced-by-count":7,"title":["KernelInterceptor"],"prefix":"10.1145","author":[{"given":"Ethel","family":"Bardsley","sequence":"first","affiliation":[]},{"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[]},{"given":"John","family":"Wickerson","sequence":"additional","affiliation":[]}],"member":"320","reference":[{"key":"key-10.1145\/2664666.2664673-1","doi-asserted-by":"crossref","unstructured":"E. Bardsley, A. Betts, N. Chong, P. Collingbourne, P. Deligiannis, A. F. Donaldson, J. Ketema, and S. Qadeer. Engineering a static verification tool for GPU kernels. InProceedings of the 26th International Conference on Computer Aided Verification (CAV '14), volume 8559 ofLecture Notes in Computer Science, pages 226--242. Springer, 2014.","DOI":"10.1007\/978-3-319-08867-9_15"},{"key":"key-10.1145\/2664666.2664673-2","doi-asserted-by":"crossref","unstructured":"A. Betts, N. Chong, A. F. Donaldson, S. Qadeer, and P. Thomson. GPUVerify: A verifier for GPU kernels. InProceedings of the ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA '12), pages 113--132. ACM, 2012.","DOI":"10.1145\/2384616.2384625"},{"key":"key-10.1145\/2664666.2664673-3","doi-asserted-by":"crossref","unstructured":"N. Chong, A. F. Donaldson, P. H. Kelly, J. Ketema, and S. Qadeer. Barrier invariants: A shared state abstraction for the analysis of data-dependent GPU kernels. InProceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA '13), pages 605--622. ACM, 2013.","DOI":"10.1145\/2509136.2509517"},{"key":"key-10.1145\/2664666.2664673-4","doi-asserted-by":"crossref","unstructured":"P. Collingbourne, C. Cadar, and P. Kelly. Symbolic crosschecking of data-parallel floating-point code.IEEE Transactions on Software Engineering, 40(7):710--737, July 2014.","DOI":"10.1109\/TSE.2013.2297120"},{"key":"key-10.1145\/2664666.2664673-5","doi-asserted-by":"crossref","unstructured":"P. Collingbourne, A. F. Donaldson, J. Ketema, and S. Qadeer. Interleaving and lock-step semantics for analysis and verification of GPU kernels. InProceedings of the 22nd European Symposium on Programming (ESOP '13), volume 7792 ofLecture Notes in Computer Science, pages 270--289. Springer, 2013.","DOI":"10.1007\/978-3-642-37036-6_16"},{"key":"key-10.1145\/2664666.2664673-6","unstructured":"E. Coumans. GPU rigid body simulation using OpenCL. In Multithreading and VFX,a tutorial atSIGGRAPH 2013, 2013. http:\/\/www.multithreadingandvfx.org\/course_notes\/GPU_rigidbody_using_OpenCL.pdf."},{"key":"key-10.1145\/2664666.2664673-7","doi-asserted-by":"crossref","unstructured":"M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants.Science of Computer Programming, 69(1--3):35--45, 2007.","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"key-10.1145\/2664666.2664673-8","unstructured":"M. Huisman and M. Mihelčić. Specification and verification of GPGPU programs using permission-based separation logic. InThe 8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE '13), 2013."},{"key":"key-10.1145\/2664666.2664673-9","doi-asserted-by":"crossref","unstructured":"A. Leung, M. Gupta, Y. Agarwal, R. Gupta, R. Jhala, and S. Lerner. Verifying GPU kernels by test amplification. InProceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '12), pages 383--394. ACM, 2012.","DOI":"10.1145\/2254064.2254110"},{"key":"key-10.1145\/2664666.2664673-10","doi-asserted-by":"crossref","unstructured":"G. Li and G. Gopalakrishnan. Scalable SMT-based verification of GPU kernel functions. InProceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE '10), pages 187--196. ACM, 2010.","DOI":"10.1145\/1882291.1882320"},{"key":"key-10.1145\/2664666.2664673-11","doi-asserted-by":"crossref","unstructured":"G. Li, P. Li, G. Sawaya, G. Gopalakrishnan, I. Ghosh, and S. P. Rajan. GKLEE: concolic verification and test generation for GPUs. InProceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPOPP '12), pages 215--224. ACM, 2012.","DOI":"10.1145\/2145816.2145844"},{"key":"key-10.1145\/2664666.2664673-12","unstructured":"J. A. Stratton, C. Rodrigrues, I.-J. Sung, N. Obeid, L. Chang, G. Liu, and W.-M. W. Hwu. Parboil: A revised benchmark suite for scientific and commercial throughput computing. Technical Report IMPACT-12-01, University of Illinois at Urbana-Champaign, Mar. 2012."}],"event":{"name":"the International Workshop","location":"Bristol, United Kingdom","acronym":"IWOCL '14","number":"2014","sponsor":["ARM","Intel","StreamComputing, StreamComputing BV","Altera Corp., Altera Corporation","AMD","Codeplay, Codeplay Software Ltd.","SAMSUNG","Imagination, Imagination Technologies Limited","QI, Qualcomm Inc."],"start":{"date-parts":[[2014,5,12]]},"end":{"date-parts":[[2014,5,13]]}},"container-title":["Proceedings of the International Workshop on OpenCL 2013 & 2014 - IWOCL '14"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2664666.2664673","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/dl.acm.org\/ft_gateway.cfm?id=2664673&ftid=1545582&dwn=1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:24Z","timestamp":1750227204000},"score":1,"resource":{"primary":{"URL":"http:\/\/dl.acm.org\/citation.cfm?doid=2664666.2664673"}},"subtitle":["automating GPU kernel verification by intercepting kernels and their parameters"],"proceedings-subject":"OpenCL 2013 & 2014","short-title":[],"issued":{"date-parts":[[2014]]},"references-count":12,"URL":"https:\/\/doi.org\/10.1145\/2664666.2664673","relation":{},"subject":[],"published":{"date-parts":[[2014]]}}}