{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T08:44:08Z","timestamp":1777106648033,"version":"3.51.4"},"reference-count":55,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"7","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/3.0\/legalcode"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2014,7]]},"DOI":"10.1109\/tse.2013.2297120","type":"journal-article","created":{"date-parts":[[2014,1,31]],"date-time":"2014-01-31T17:52:28Z","timestamp":1391190748000},"page":"710-737","source":"Crossref","is-referenced-by-count":18,"title":["Symbolic Crosschecking of Data-Parallel Floating-Point Code"],"prefix":"10.1109","volume":"40","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":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349320"},{"key":"ref33","year":"0"},{"key":"ref32","year":"0"},{"key":"ref31","year":"0"},{"key":"ref30","year":"0"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"ref36","year":"0"},{"key":"ref35","year":"0"},{"key":"ref34","year":"0"},{"key":"ref28","year":"0"},{"key":"ref27","year":"0"},{"key":"ref29","year":"0"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268974"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2003.1252469"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542490"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/1964218.1964221"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"ref24","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-19861-8_16","article-title":"A Static Task Partitioning Approach for Heterogeneous Systems Using OpenCL","author":"grewe","year":"2011","journal-title":"Proc 20th Int?l Conf Compiler Construction (CC ?11)"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190226"},{"key":"ref26","year":"0"},{"key":"ref25","first-page":"629","article-title":"Floating-Point Verification","volume":"13","author":"harrison","year":"2007","journal-title":"J Universal Computer Science"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/268998.266641"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146256"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1145\/1941553.1941574"},{"key":"ref54","article-title":"Checking Non-Interference in SPMD Programs","author":"tripakis","year":"2010","journal-title":"Proc Second USENIX Workshop Hot Topics in Parallelism (HotPar ?10)"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2000.878283"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.10"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966463"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882320"},{"key":"ref11","article-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs","author":"cadar","year":"2008","journal-title":"Proc USENIX Symp Operating Systems Design and Implementation (OSDI)"},{"key":"ref12","article-title":"Phi-Predication for Light-Weight If-Conversion","author":"chuang","year":"2003","journal-title":"Proc Int?l Symp Code Generation and Optimization Feedback-Directed and Runtime Optimization (CGO ?03)"},{"key":"ref13","year":"0"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/1119772.1119831"},{"key":"ref15","article-title":"Symbolic Testing of OpenCL Code","author":"collingbourne","year":"2011","journal-title":"Proc Haifa Verification Conference (HVC)"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966475"},{"key":"ref17","year":"0"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/s10766-005-0004-8"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996853"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384625"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73561"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_27"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2007.20"},{"key":"ref8","article-title":"Automated Dynamic Analysis of CUDA Programs","author":"boyer","year":"2008","journal-title":"Proceedings of Third Workshop on Software Tools for MultiCore Systems (STMCS) 2008"},{"key":"ref49","doi-asserted-by":"crossref","DOI":"10.1145\/781498.781528","article-title":"Hybrid Dynamic Data Race Detection","author":"o?callahan","year":"2003","journal-title":"Proc Ninth ACM Symp Principles and Practice of Parallel Programming (PPoPP ?03)"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.333"},{"key":"ref9","author":"bradski","year":"2008","journal-title":"Learning OpenCV Computer Vision With the OpenCV Library"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/951710.951714"},{"key":"ref45","year":"0"},{"key":"ref48","year":"0"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"ref42","year":"0"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/2145816.2145844"},{"key":"ref44","article-title":"Exact Projection Functions for Floating Point Number Constraints","author":"michel","year":"2002","journal-title":"Proc Seventh Int'l Symp Artificial Intelligence and Mathematics (AMAI ?02)"},{"key":"ref43","article-title":"Reducing Test Inputs Using Information Partitions","author":"majumdar","year":"2009","journal-title":"Proc 21st Int?l Conf Computer-Aided Verification (CAV ?09)"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/ieeexplore.ieee.org\/iel7\/32\/6848876\/06698391.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/6848876\/06698391.pdf?arnumber=6698391","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,10]],"date-time":"2023-07-10T05:02:29Z","timestamp":1688965349000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6698391\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":55,"journal-issue":{"issue":"7"},"URL":"https:\/\/doi.org\/10.1109\/tse.2013.2297120","relation":{},"ISSN":["0098-5589","1939-3520"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7]]}}}