{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:57:31Z","timestamp":1770296251052,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642341878","type":"print"},{"value":"9783642341885","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34188-5_18","type":"book-chapter","created":{"date-parts":[[2012,10,11]],"date-time":"2012-10-11T14:04:33Z","timestamp":1349964273000},"page":"203-218","source":"Crossref","is-referenced-by-count":40,"title":["Symbolic Testing of OpenCL Code"],"prefix":"10.1007","author":[{"given":"Peter","family":"Collingbourne","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristian","family":"Cadar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul H. J.","family":"Kelly","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","unstructured":"Boyer, M., Skadron, K., Weimer, W.: Automated dynamic analysis of CUDA programs. In: STMCS 2008 (April 2008)"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: EuroSys 2011 (April 2011)","DOI":"10.1145\/1966445.1966463"},{"key":"18_CR3","unstructured":"clang: a C language family frontend for LLVM, \n                    \n                      http:\/\/clang.llvm.org\/"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D.: Hardware verification using ANSI-C programs as a reference. In: ASP-DAC 2003 (January 2003)","DOI":"10.1145\/1119772.1119831"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Collingbourne, P., Cadar, C., Kelly, P.H.: Symbolic crosschecking of floating-point and SIMD code. In: EuroSys 2011 (April 2011)","DOI":"10.1145\/1966445.1966475"},{"key":"18_CR6","unstructured":"Coumans, E., et al.: Bullet continuous collision detection and physics library, \n                    \n                      http:\/\/bulletphysics.org\/"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: Fasttrack: Efficient and precise dynamic race detection. In: PLDI 2009 (June 2009)","DOI":"10.1145\/1542476.1542490"},{"issue":"4","key":"18_CR8","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/1964218.1964221","volume":"38","author":"M.B. Giles","year":"2011","unstructured":"Giles, M.B., Mudalige, G.R., Sharif, Z., Markall, G.R., Kelly, P.H.J.: Performance analysis of the OP2 framework on many-core architectures. SIGMETRICS Performance Evaluation Review\u00a038(4), 9\u201315 (2011)","journal-title":"SIGMETRICS Performance Evaluation Review"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-19861-8_16","volume-title":"Compiler Construction","author":"D. Grewe","year":"2011","unstructured":"Grewe, D., O\u2019Boyle, M.F.P.: A Static Task Partitioning Approach for Heterogeneous Systems Using OpenCL. In: Knoop, J. (ed.) CC 2011. LNCS, vol.\u00a06601, pp. 286\u2013305. Springer, Heidelberg (2011)"},{"key":"18_CR10","unstructured":"IMPACT Research Group, UIUC. Parboil benchmark suite, \n                    \n                      http:\/\/impact.crhc.illinois.edu\/parboil.php"},{"key":"18_CR11","unstructured":"International Organization for Standardization. ISO\/IEC\u00a09899-1999: Programming Languages\u2014C (December 1999)"},{"key":"18_CR12","unstructured":"Khronos OpenCL Working Group. The OpenCL Specification, version 1.1, revision 36 (September 2010)"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"King, J.C.: A new approach to program testing. In: ICRS 1975 (April 1975)","DOI":"10.1145\/800027.808444"},{"key":"18_CR14","unstructured":"Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: CGO 2004 (March 2004)"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: FSE 2010 (November 2010)","DOI":"10.1145\/1882291.1882320"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Li, G., Li, P., Sawaya, G., Ghosh, I.: GKLEE: Concolic verification and test generation for GPUs. In: PPoPP 2012 (Februery 2012)","DOI":"10.1145\/2145816.2145844"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI 2000 (May 2000)","DOI":"10.1145\/349299.349314"},{"key":"18_CR18","unstructured":"NVIDIA. NVIDIA CUDA Programming Guide, Version 3.0 (February 2010)"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"O\u2019Callahan, R., Choi, J.-D.: Hybrid dynamic data race detection. In: PPoPP 2003 (June 2003)","DOI":"10.1145\/781527.781528"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Person, S., Dwyer, M.B., Elbaum, S., P\u01ces\u01cereanu, C.S.: Differential symbolic execution. In: FSE 2008 (November 2008)","DOI":"10.1145\/1453101.1453131"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: A dynamic data race detector for multithreaded programs. In: SOSP 1997 (October 1997)","DOI":"10.1145\/265924.265927"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: ISSTA 2006 (July 2006)","DOI":"10.1145\/1146238.1146256"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Smith, E.W., Dill, D.L.: Automatic formal verification of block cipher implementations. In: FMCAD 2008 (November 2008)","DOI":"10.1109\/FMCAD.2008.ECP.10"},{"key":"18_CR24","unstructured":"Tripakis, S., Stergiou, C., Lublinerman, R.: Checking non-interference in SPMD programs. In: HotPar 2010 (June 2010)"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Zheng, M., Ravi, V.T., Qin, F., Agrawal, G.: GRace: A low-overhead mechanism for detecting data races in GPU programs. In: PPoPP 2011 (February 2011)","DOI":"10.1145\/1941553.1941574"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34188-5_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:47:31Z","timestamp":1620132451000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34188-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642341878","9783642341885"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34188-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}