{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:50Z","timestamp":1772164010112,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":7,"publisher":"ACM","license":[{"start":{"date-parts":[[2010,1,9]],"date-time":"2010-01-09T00:00:00Z","timestamp":1262995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2010,1,9]]},"DOI":"10.1145\/1693453.1693512","type":"proceedings-article","created":{"date-parts":[[2010,1,12]],"date-time":"2010-01-12T15:23:12Z","timestamp":1263309792000},"page":"357-358","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A symbolic verifier for CUDA programs"],"prefix":"10.1145","author":[{"given":"Guodong","family":"Li","sequence":"first","affiliation":[{"name":"University of Utah, Salt Lake City, UT, USA"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, UT, USA"}]},{"given":"Robert M.","family":"Kirby","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, UT, USA"}]},{"given":"Dan","family":"Quinlan","sequence":"additional","affiliation":[{"name":"Lawrence Livermore National Laboratory, Livermore, CA, USA"}]}],"member":"320","published-online":{"date-parts":[[2010,1,9]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"M. Boyer K. Skadron and W.Weimer. Automated Dynamic Analysis of CUDA Programs. http:\/\/www.cs.virginia.edu\/~mwb7w\/cuda\/.  M. Boyer K. Skadron and W.Weimer. Automated Dynamic Analysis of CUDA Programs. http:\/\/www.cs.virginia.edu\/~mwb7w\/cuda\/."},{"key":"e_1_3_2_1_2_1","unstructured":"CUDA Zone. http:\/\/www.nvidia.com\/object\/cuda home.html.  CUDA Zone. http:\/\/www.nvidia.com\/object\/cuda home.html."},{"key":"e_1_3_2_1_3_1","unstructured":"Yices: An SMT Solver. http:\/\/yices.csl.sri.com.  Yices: An SMT Solver. http:\/\/yices.csl.sri.com."},{"key":"e_1_3_2_1_4_1","unstructured":"The ROSE Compiler. http:\/\/www.rosecompiler.org\/.  The ROSE Compiler. http:\/\/www.rosecompiler.org\/."},{"key":"e_1_3_2_1_5_1","first-page":"2009","author":"Lublinerman R.","year":"2009","unstructured":"R. Lublinerman and S. Tripakis , Checking Equivalence of SPMD Programs Using Non-Interference. http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/ 2009 \/EECS- 2009 - 2042 .html. R. Lublinerman and S. Tripakis, Checking Equivalence of SPMD Programs Using Non-Interference. http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/2009\/EECS-2009-42.html.","journal-title":"Checking Equivalence of SPMD Programs Using Non-Interference. http:\/\/www.eecs.berkeley.edu\/Pubs\/TechRpts\/"},{"key":"e_1_3_2_1_6_1","unstructured":"Bounded Model Checking for ANSI-C. http:\/\/www.cprover.org\/cbmc\/.  Bounded Model Checking for ANSI-C. http:\/\/www.cprover.org\/cbmc\/."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_9"}],"event":{"name":"PPoPP '10: ACM SIGPLAN Principles and Practice of Parallel Computing","location":"Bangalore India","acronym":"PPoPP '10","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 15th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1693453.1693512","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1693453.1693512","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:45:35Z","timestamp":1750236335000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1693453.1693512"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,9]]},"references-count":7,"alternative-id":["10.1145\/1693453.1693512","10.1145\/1693453"],"URL":"https:\/\/doi.org\/10.1145\/1693453.1693512","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1837853.1693512","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2010,1,9]]},"assertion":[{"value":"2010-01-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}