{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T09:59:42Z","timestamp":1740131982886,"version":"3.37.3"},"reference-count":62,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"7","license":[{"start":{"date-parts":[[2018,7,1]],"date-time":"2018-07-01T00:00:00Z","timestamp":1530403200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"EU FP7 STREP project CARP","award":["287767"],"award-info":[{"award-number":["287767"]}]},{"name":"EPSRC PSL","award":["EP\/I006761\/1"],"award-info":[{"award-number":["EP\/I006761\/1"]}]},{"name":"Imperial College London\u2019s EPSRC Impact Acceleration Account"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2018,7,1]]},"DOI":"10.1109\/tse.2017.2718516","type":"journal-article","created":{"date-parts":[[2017,6,22]],"date-time":"2017-06-22T18:40:23Z","timestamp":1498156823000},"page":"631-650","source":"Crossref","is-referenced-by-count":1,"title":["Implementing and Evaluating Candidate-Based Invariant Generation"],"prefix":"10.1109","volume":"44","author":[{"given":"Adam","family":"Betts","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nathan","family":"Chong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pantazis","family":"Deligiannis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7448-7961","authenticated-orcid":false,"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeroen","family":"Ketema","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"article-title":"Translation validation for the PENCIL $\\rightarrow$\n OpenCL compiler","year":"2014","author":"donaldson","key":"ref39"},{"key":"ref38","first-page":"138","article-title":"PENCIL: A platform-neutral compute\n intermediate language for accelerator programming","author":"baghdadi","year":"2015","journal-title":"Proc Int Conf Parallel Archit Compil"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2400682.2400713"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/1735688.1735702"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/IISWC.2009.5306797"},{"article-title":"Parboil: A revised benchmark suite for\n scientific and commercial throughput computing","year":"2012","author":"stratton","key":"ref30"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/2664666.2664673"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509517"},{"year":"2014","key":"ref35","article-title":"Basemark CL"},{"article-title":"PolyPench\/C: The polyhedral benchmark suite","year":"2015","author":"pouchet","key":"ref34"},{"key":"ref60","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1145\/605466.605469","article-title":"Invariant inference for static checking","volume":"27","author":"nimmer","year":"2002","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"ref62","article-title":"Prefix sums and their applications","author":"blelloch","year":"1990","journal-title":"Synthesis of Parallel Algorithms"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572284"},{"year":"2014","key":"ref28","article-title":"C++ AMP sample projects for download (MSDN blog)"},{"year":"2014","key":"ref27","article-title":"GPU Computing SDK"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/ISPASS.2009.4919648"},{"key":"ref2","first-page":"634","article-title":"Invgen: An efficient invariant generator","author":"gupta","year":"2009","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref1","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning meanings to programs","volume":"19","author":"floyd","year":"1967","journal-title":"Math Aspects Comput Sci"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2743017"},{"key":"ref22","first-page":"1","article-title":"The GPUVerify method: A tutorial overview","author":"donaldson","year":"2014","journal-title":"Proceedings of the 15th International Workshop on Automated Verification of Critical Systems"},{"article-title":"BoogiePL: A typed procedural language for checking object-oriented programs","year":"2005","author":"deline and","key":"ref21"},{"key":"ref24","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"2008","journal-title":"Proc Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref23","first-page":"364","article-title":"Boogie: A modular reusable verifier for object-oriented programs","author":"barnett","year":"2005","journal-title":"Proc Second Int l Symp Formal Methods for Components and Objects"},{"year":"2014","key":"ref26","article-title":"Accelerated parallel processing SDK"},{"key":"ref25","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","article-title":"CVC4","author":"barrett","year":"2011","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882320"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/2851613.2851830"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0095-0"},{"key":"ref58","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/978-3-642-31424-7_32","article-title":"A solver for\n reachability modulo theories","author":"lal","year":"2012","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref57","first-page":"72","article-title":"Construction of abstract state graphs with PVS","author":"graf","year":"1997","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_5"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.03.013"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2013.2297120"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1145\/2145816.2145844"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.21236\/ADA538815"},{"key":"ref10","first-page":"443","article-title":"Inductive invariant generation via\n abductive inference","author":"dillig","year":"2013","journal-title":"Proc ACM SIGPLAN Int Conf Object Oriented Program Syst Languages Appl"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535843"},{"key":"ref40","first-page":"230","article-title":"Warps and atomics: Beyond barrier synchronisation in the verification of GPU\n kernels","author":"barsdley","year":"2014","journal-title":"Proc 6th NASA Formal Methods Symp"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00196-4"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384625"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1508244.1508275"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1108792.1108813"},{"journal-title":"CUDA C Programming Guide Version 5 5","year":"2013","key":"ref17"},{"journal-title":"The OpenCL Specification version 2 0","year":"2013","key":"ref18"},{"key":"ref19","first-page":"270","article-title":"Interleaving and lock-step semantics for\n analysis and verification of GPU kernels","author":"collingbourne","year":"2013","journal-title":"Proc Eur Conf Program Languages Syst"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"ref3","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","article-title":"Finding loop invariants for programs over arrays using a theorem prover","author":"kov\u00e1cs","year":"2009","journal-title":"Proc 16th Int Conf Fundam Approaches Softw Eng"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.1998.655922"},{"key":"ref5","first-page":"500","article-title":"Houdini, an annotation assistant for ESC\/Java","author":"flanagan","year":"2001","journal-title":"Proc Int 7 Symp Formal Methods Europe on Formal Methods for Increasing Software Productivity"},{"key":"ref8","first-page":"15","article-title":"PostHat and all that: Automating abstract\n interpretation","author":"thakur","year":"2013","journal-title":"Proc 4th Workshop Tools Automatic Program Anal"},{"key":"ref7","first-page":"661","article-title":"Apron: A library of numerical abstract domains for static analysis","author":"jeannet","year":"2009","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254110"},{"key":"ref9","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/11817963_14","article-title":"Lazy abstraction with interpolants","author":"mcmillan","year":"2006","journal-title":"Proc Int Conf Comput -Aided Verification"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00196-4"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1111\/j.1469-8137.1912.tb05611.x"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/1941553.1941574"},{"year":"2017","key":"ref47","article-title":"CUDA-MEMCHECK"},{"key":"ref42","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","article-title":"A tool for\n checking ANSI-C programs","author":"clarke","year":"2004","journal-title":"Proc Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref41","first-page":"1","article-title":"Schedule trees","author":"verdoolaege","year":"2014","journal-title":"Proceedings of the 4th International Workshop on Polyhedral Compilation Techniques"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2016.11"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40787-1_15"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/8411354\/07955079.pdf?arnumber=7955079","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T13:35:04Z","timestamp":1643204104000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/7955079\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,1]]},"references-count":62,"journal-issue":{"issue":"7"},"URL":"https:\/\/doi.org\/10.1109\/tse.2017.2718516","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"type":"print","value":"0098-5589"},{"type":"electronic","value":"1939-3520"},{"type":"electronic","value":"2326-3881"}],"subject":[],"published":{"date-parts":[[2018,7,1]]}}}