{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T01:11:41Z","timestamp":1780708301350,"version":"3.54.1"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319088662","type":"print"},{"value":"9783319088679","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08867-9_15","type":"book-chapter","created":{"date-parts":[[2014,6,28]],"date-time":"2014-06-28T07:37:30Z","timestamp":1403941050000},"page":"226-242","source":"Crossref","is-referenced-by-count":30,"title":["Engineering a Static Verification Tool for GPU Kernels"],"prefix":"10.1007","author":[{"given":"Ethel","family":"Bardsley","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Adam","family":"Betts","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nathan","family":"Chong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"Collingbourne","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pantazis","family":"Deligiannis","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeroen","family":"Ketema","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniel","family":"Liew","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Allen, J., Kennedy, K., Porterfield, C., Warren, J.: Conversion of control dependence to data dependence. In: POPL, pp. 177\u2013189 (1983)","DOI":"10.1145\/567067.567085"},{"key":"15_CR2","unstructured":"AMD: AMD Accelerated Parallel Processing (APP) SDK, http:\/\/developer.amd.com\/sdks\/amdappsdk"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Bakhoda, A., Yuan, G.L., Fung, W.W.L., Wong, H., Aamodt, T.M.: Analyzing CUDA workloads using a detailed gpu simulator. In: ISPASS, pp. 163\u2013174 (2009)","DOI":"10.1109\/ISPASS.2009.4919648"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-319-06200-6_18","volume-title":"NASA Formal Methods","author":"E. Bardsley","year":"2014","unstructured":"Bardsley, E., Donaldson, A.F.: Warps and atomics: Beyond barrier synchronization in the verification of GPU kernels. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol.\u00a08430, pp. 230\u2013245. Springer, Heidelberg (2014)"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Bardsley, E., Donaldson, A.F., Wickerson, J.: KernelInterceptor: Automating gpu kernel verification by intercepting kernels and their parameters. In: IWOCL (2014)","DOI":"10.1145\/2664666.2664673"},{"key":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Betts, A., Chong, N., Donaldson, A.F., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: OOPSLA, pp. 113\u2013132 (2012)","DOI":"10.1145\/2384616.2384625"},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Che, S., et al.: Rodinia: A benchmark suite for heterogeneous computing. In: Workload Characterization, pp. 44\u201354 (2009)","DOI":"10.1109\/IISWC.2009.5306797"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-642-38088-4_15","volume-title":"NASA Formal Methods","author":"W.-F. Chiang","year":"2013","unstructured":"Chiang, W.-F., Gopalakrishnan, G., Li, G., Rakamari\u0107, Z.: Formal analysis of GPU programs with atomics via conflict-directed delay-bounding. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol.\u00a07871, pp. 213\u2013228. Springer, Heidelberg (2013)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Chong, N., Donaldson, A.F., Kelly, P., Ketema, J., Qadeer, S.: Barrier invariants: a shared state abstraction for the analysis of data-dependent GPU kernels. In: OOPSLA (2013)","DOI":"10.1145\/2509136.2509517"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Chong, N., Donaldson, A.F., Ketema, J.: A sound and complete abstraction for reasoning about parallel prefix sums. In: POPL, pp. 397\u2013410 (2014)","DOI":"10.1145\/2535838.2535882"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Formal Methods in Computer-Aided Design","author":"C.-T. Chou","year":"2004","unstructured":"Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 382\u2013398. Springer, Heidelberg (2004)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Collingbourne, P., Cadar, C., Kelly, P.H.J.: Symbolic crosschecking of data-parallel floating-point code. IEEE Trans. Software Eng. (to appear, 2014)","DOI":"10.1109\/TSE.2013.2297120"},{"key":"15_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-642-37036-6_16","volume-title":"Programming Languages and Systems","author":"P. Collingbourne","year":"2013","unstructured":"Collingbourne, P., Donaldson, A.F., Ketema, J., Qadeer, S.: Interleaving and lock-step semantics for analysis and verification of GPU kernels. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. LNCS, vol.\u00a07792, pp. 270\u2013289. Springer, Heidelberg (2013)"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Danalis, A., et al.: The scalable heterogeneous computing (SHOC) benchmark suite. In: GPGPU 2010, pp. 63\u201374 (2010)","DOI":"10.1145\/1735688.1735702"},{"issue":"1","key":"15_CR17","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s10703-011-0124-2","volume":"39","author":"A.F. Donaldson","year":"2011","unstructured":"Donaldson, A.F., Kroening, D., R\u00fcmmer, P.: Automatic analysis of DMA races using model checking and k-induction. Formal Methods in System Design\u00a039(1), 83\u2013113 (2011)","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"15_CR18","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/24039.24041","volume":"9","author":"J. Ferrante","year":"1987","unstructured":"Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst.\u00a09(3), 319\u2013349 (1987)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J.-C. Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. LNCS, vol.\u00a07792, pp. 125\u2013128. Springer, Heidelberg (2013)"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., M. Leino, K.R.: Houdini, an annotation assistant for eSC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"15_CR21","doi-asserted-by":"crossref","unstructured":"Grauer-Gray, S., Xu, L., Searles, R., Ayalasomayajula, S., Cavazos, J.: Auto-tuning a high-level language targeted to GPU codes. In: InPar (2012)","DOI":"10.1109\/InPar.2012.6339595"},{"key":"15_CR22","unstructured":"Harris, M., Buck, I.: GPU flow-control idioms. In: GPU Gems\u00a02. Addison-Wesley (2005)"},{"key":"15_CR23","unstructured":"Huisman, M., Mihel\u010di\u0107, M.: Specification and verification of GPGPU programs using permission-based separation logic. In: BYTECODE (2013)"},{"key":"15_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-28652-0_1","volume-title":"Compiler Construction","author":"R. Karrenberg","year":"2012","unstructured":"Karrenberg, R., Hack, S.: Improving performance of openCL on cPUs. In: O\u2019Boyle, M. (ed.) CC 2012. LNCS, vol.\u00a07210, pp. 1\u201320. Springer, Heidelberg (2012)"},{"key":"15_CR25","unstructured":"Khronos OpenCL Working Group: The OpenCL specification, version 2.0 (2013)"},{"key":"15_CR26","doi-asserted-by":"crossref","unstructured":"Leung, A., Gupta, M., Agarwal, Y., et al.: Verifying GPU kernels by test amplification. In: PLDI, pp. 383\u2013394 (2012)","DOI":"10.1145\/2254064.2254110"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: FSE, pp. 187\u2013196 (2010)","DOI":"10.1145\/1882291.1882320"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Li, G., Li, P., Sawaya, G., Gopalakrishnan, G., Ghosh, I., Rajan, S.P.: GKLEE: Concolic verification and test generation for GPUs. In: PPoPP, pp. 215\u2013224 (2012)","DOI":"10.1145\/2370036.2145844"},{"key":"15_CR29","doi-asserted-by":"crossref","unstructured":"Li, P., Li, G., Gopalakrishnan, G.: Parametric flows: Automated behavior equivalencing for symbolic analysis of races in CUDA programs. In: SC, pp. 29:1\u201329:10 (2012)","DOI":"10.1109\/SC.2012.94"},{"key":"15_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"1999","unstructured":"McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 219\u2013237. Springer, Heidelberg (1999)"},{"key":"15_CR31","unstructured":"Microsoft Corporation: C++ AMP sample projects for download (MSDN blog), http:\/\/blogs.msdn.com\/b\/nativeconcurrency\/archive\/2012\/01\/30\/c-amp-sample-projects-for-download.aspx"},{"key":"15_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"15_CR33","unstructured":"NVIDIA: CUDA C programming guide, version 5.5 (2013)"},{"key":"15_CR34","unstructured":"NVIDIA: GPU Computing SDK (accessed 2013), https:\/\/developer.nvidia.com\/gpu-computing-sdk"},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"Rakamaric, Z., Hu, A.J.: Automatic inference of frame axioms using static analysis. In: ASE, pp. 89\u201398 (2008)","DOI":"10.1109\/ASE.2008.19"},{"key":"15_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-93900-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z. Rakamari\u0107","year":"2009","unstructured":"Rakamari\u0107, Z., Hu, A.J.: A scalable memory model for low-level code. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 290\u2013304. Springer, Heidelberg (2009)"},{"key":"15_CR37","unstructured":"Rightware Oy: Basemark CL, http:\/\/www.rightware.com\/benchmarking-software\/basemark-cl\/"},{"key":"15_CR38","unstructured":"Stratton, J., et al.: Parboil: A revised benchmark suite for scientific and commercial throughput computing. Tech. Rep. IMPACT-12-01, UIUC (2012)"},{"key":"15_CR39","doi-asserted-by":"crossref","unstructured":"Talupur, M., Tuttle, M.R.: Going with the flow: Parameterized verification using message flows. In: FMCAD, pp. 1\u20138 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.14"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08867-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,11]],"date-time":"2019-08-11T20:49:11Z","timestamp":1565556551000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08867-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319088662","9783319088679"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08867-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}