{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:40:01Z","timestamp":1780994401098,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642370359","type":"print"},{"value":"9783642370366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-37036-6_16","type":"book-chapter","created":{"date-parts":[[2013,2,18]],"date-time":"2013-02-18T19:35:55Z","timestamp":1361216155000},"page":"270-289","source":"Crossref","is-referenced-by-count":30,"title":["Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels"],"prefix":"10.1007","author":[{"given":"Peter","family":"Collingbourne","sequence":"first","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":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Pearson Education, 2nd edn. (2007)"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Allen, J., Kennedy, K., Porterfield, C., Warren, J.: Conversion of control dependence to data dependence. In: POPL 1983, pp. 177\u2013189 (1983)","DOI":"10.1145\/567067.567085"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Alshawabkeh, M., Jang, B., Kaeli, D.: Accelerating the local outlier factor algorithm on a GPU for intrusion detection systems. In: GPGPU-3, pp. 104\u2013110 (2010)","DOI":"10.1145\/1735688.1735707"},{"key":"16_CR4","unstructured":"AMD: AMD Accelerated Parallel Processing (APP) SDK, http:\/\/developer.amd.com\/sdks\/amdappsdk\/pages\/default.aspx"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: PASTE 2005, pp. 82\u201387 (2005)","DOI":"10.1145\/1108768.1108813"},{"key":"16_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., Leino, K.R.M.: 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":"16_CR7","doi-asserted-by":"crossref","unstructured":"Betts, A., Chong, N., Donaldson, A.F., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: OOPSLA 2012, pp. 113\u2013132 (2012)","DOI":"10.1145\/2398857.2384625"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-642-34188-5_18","volume-title":"Hardware and Software: Verification and Testing","author":"P. Collingbourne","year":"2012","unstructured":"Collingbourne, P., Cadar, C., Kelly, P.H.J.: Symbolic Testing of OpenCL Code. In: Eder, K., Louren\u00e7o, J., Shehory, O. (eds.) HVC 2011. LNCS, vol.\u00a07261, pp. 203\u2013218. Springer, Heidelberg (2012)"},{"issue":"1","key":"16_CR9","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/322169.322180","volume":"27","author":"R.A. DeMillo","year":"1980","unstructured":"DeMillo, R.A., Eisenstat, S.C., Lipton, R.J.: Space-time trade-offs in structured programming: An improved combinatorial embedding theorem. J. ACM\u00a027(1), 123\u2013127 (1980)","journal-title":"J. ACM"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Fung, W.W., Sham, I., Yuan, G., Aamodt, T.M.: Dynamic warp formation and scheduling for efficient GPU control flow. In: MICRO 2007, pp. 407\u2013418 (2007)","DOI":"10.1109\/MICRO.2007.4408272"},{"key":"16_CR11","unstructured":"Habermaier, A.: The model of computation of CUDA and its formal semantics. Tech. Rep. 2011-14, University of Augsburg (2011)"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-642-28869-2_16","volume-title":"Programming Languages and Systems","author":"A. Habermaier","year":"2012","unstructured":"Habermaier, A., Knapp, A.: On the Correctness of the SIMT Execution Model of GPUs. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol.\u00a07211, pp. 316\u2013335. Springer, Heidelberg (2012)"},{"key":"16_CR13","unstructured":"Khronos Group: The OpenCL specification, version 1.2 (2011)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Lamport, L.: What good is temporal logic? In: Information Processing 1983, pp. 657\u2013668 (1983)","DOI":"10.1145\/2402.322398"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Leung, A., Gupta, M., Agarwal, Y., Gupta, R., Jhala, R., Lerner, S.: Verifying GPU kernels by test amplification. In: PLDI 2012, pp. 383\u2013394 (2012)","DOI":"10.1145\/2345156.2254110"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: FSE 2010, pp. 187\u2013196 (2010)","DOI":"10.1145\/1882291.1882320"},{"key":"16_CR17","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 2012, pp. 215\u2013224 (2012)","DOI":"10.1145\/2370036.2145844"},{"key":"16_CR18","unstructured":"Microsoft Corporation: C++ AMP sample projects for download, http:\/\/blogs.msdn.com\/b\/nativeconcurrency\/archive\/2012\/01\/30\/c-amp-sample-projects-for-download.aspx"},{"key":"16_CR19","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.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"16_CR20","unstructured":"NVIDIA: CUDA Toolkit Release Archive, http:\/\/developer.nvidia.com\/cuda\/cuda-toolkit-archive"},{"key":"16_CR21","unstructured":"NVIDIA: NVIDIA CUDA C Programming Guide, Version 4.2 (2012)"},{"key":"16_CR22","unstructured":"Rightware Oy: Basemark CL, http:\/\/www.rightware.com\/en\/Benchmarking+Software\/Basemark%99+CL"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Zhu, F., Chen, P., Yang, D., Zhang, W., Chen, H., Zang, B.: A GPU-based high-throughput image retrieval algorithm. In: GPGPU-5, pp. 30\u201337 (2012)","DOI":"10.1145\/2159430.2159434"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-37036-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,8]],"date-time":"2022-02-08T22:07:47Z","timestamp":1644358067000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-37036-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642370359","9783642370366"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-37036-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}