{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:35:09Z","timestamp":1750221309636,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,11,12]],"date-time":"2017-11-12T00:00:00Z","timestamp":1510444800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/L000407\/1"],"award-info":[{"award-number":["EP\/L000407\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-AC02-06CH11357"],"award-info":[{"award-number":["DE-AC02-06CH11357"]}],"id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,11,12]]},"DOI":"10.1145\/3145344.3145488","type":"proceedings-article","created":{"date-parts":[[2017,10,31]],"date-time":"2017-10-31T12:31:37Z","timestamp":1509453097000},"page":"42-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards Self-Verification in Finite Difference Code Generation"],"prefix":"10.1145","author":[{"given":"Jan","family":"H\u00fcckelheim","sequence":"first","affiliation":[{"name":"Imperial College London, London, UK"}]},{"given":"Ziqing","family":"Luo","sequence":"additional","affiliation":[{"name":"University of Delaware, Newark, DE, USA"}]},{"given":"Fabio","family":"Luporini","sequence":"additional","affiliation":[{"name":"Imperial College London, London, UK"}]},{"given":"Navjot","family":"Kukreja","sequence":"additional","affiliation":[{"name":"Imperial College London, London, UK"}]},{"given":"Michael","family":"Lange","sequence":"additional","affiliation":[{"name":"Imperial College London, London, UK"}]},{"given":"Gerard","family":"Gorman","sequence":"additional","affiliation":[{"name":"Imperial College London, London, UK"}]},{"given":"Stephen","family":"Siegel","sequence":"additional","affiliation":[{"name":"University of Delaware, Newark, DE, USA"}]},{"given":"Matthew","family":"Dwyer","sequence":"additional","affiliation":[{"name":"University of Nebraska, Lincoln, NE, USA"}]},{"given":"Paul","family":"Hovland","sequence":"additional","affiliation":[{"name":"Argonne National Laboratory, Lemont, IL, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,11,12]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Accessed","author":"IEEE POSIX","year":"1995","unstructured":"IEEE POSIX 1003.1c standard. 1995 . POSIX Threads. http:\/\/www.unix.org\/version3\/ieee_std.html. (1995) . Accessed Oct. 30, 2015. IEEE POSIX 1003.1c standard. 1995. POSIX Threads. http:\/\/www.unix.org\/version3\/ieee_std.html. (1995). Accessed Oct. 30, 2015."},{"key":"e_1_3_2_1_2_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"1986","unstructured":"Alfred V. Aho , Ravi Sethi , and Jeffrey D . Ullman . 1986 . Compilers, Principles, Techniques , and Tools. Addison-Wesley . Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. 1986. Compilers, Principles, Techniques, and Tools. Addison-Wesley."},{"key":"e_1_3_2_1_3_1","volume-title":"Simflowny 2: An upgraded platform for scientific modeling and simulation. arXiv preprint arXiv:1702.04715","author":"Arbona A","year":"2017","unstructured":"A Arbona , B Mi\u00f1ano , A Rigo , C Bona , C Palenzuela , A Artigues , C Bona-Casas , and J Mass\u00f3 . 2017. Simflowny 2: An upgraded platform for scientific modeling and simulation. arXiv preprint arXiv:1702.04715 ( 2017 ). A Arbona, B Mi\u00f1ano, A Rigo, C Bona, C Palenzuela, A Artigues, C Bona-Casas, and J Mass\u00f3. 2017. Simflowny 2: An upgraded platform for scientific modeling and simulation. arXiv preprint arXiv:1702.04715 (2017)."},{"key":"e_1_3_2_1_4_1","volume-title":"CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.)","volume":"8044","author":"Barnat Jiri","year":"2013","unstructured":"Jiri Barnat , Lubos Brim , Vojtech Havel , Jan Havl\u00edcek , Jan Kriho , Milan Lenco , Petr Rockai , Vladim\u00edr Still , and Jir\u00ed Weiser . 2013 . DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs. In Computer Aided Verification - 25th International Conference , CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.) , Vol. 8044 . Springer, 863--868. Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havl\u00edcek, Jan Kriho, Milan Lenco, Petr Rockai, Vladim\u00edr Still, and Jir\u00ed Weiser. 2013. DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 863--868."},{"key":"e_1_3_2_1_5_1","volume-title":"4th International Symposium, FMCO 2005","author":"Barnett Michael","year":"2005","unstructured":"Michael Barnett , Bor-Yuh Evan Chang , Robert DeLine , Bart Jacobs , and K. Rustan M. Leino . 2005 . Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects , 4th International Symposium, FMCO 2005 , Amsterdam, The Netherlands , November 1-4, 2005, Revised Lectures (Lecture Notes in Computer Science), Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.), Vol. 4111. Springer, 364--387. Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. 2005. Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures (Lecture Notes in Computer Science), Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem P. de Roever (Eds.), Vol. 4111. Springer, 364--387."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2743017"},{"key":"e_1_3_2_1_7_1","unstructured":"Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroclaw Poland 53--64. http:\/\/proval.lri.fr\/publications\/boogie11final.pdf  Fran\u00e7ois Bobot Jean-Christophe Filli\u00e2tre Claude March\u00e9 and Andrei Paskevich. 2011. Why3: Shepherd Your Herd of Provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages. Wroclaw Poland 53--64. http:\/\/proval.lri.fr\/publications\/boogie11final.pdf"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.camwa.2014.06.004"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993545"},{"key":"e_1_3_2_1_10_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs . In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08) . USENIX Association, Berkeley, CA, USA, 209--224. http:\/\/dl.acm.org\/citation.cfm?id= 1855741.1855756 Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08). USENIX Association, Berkeley, CA, USA, 209--224. http:\/\/dl.acm.org\/citation.cfm?id=1855741.1855756"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/377792.377807"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491453"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60761-7"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"G. Gopalakrishnan P. D. Hovland C. Iancu S. Krishnamoorthy I. Laguna R. A. Lethin K. Sen S. F. Siegel and A. Solar-Lezama. 2017. Report of the HPC Correctness Summit Jan 25--26 2017 Washington DC. ArXiv e-prints (May 2017). arXiv:cs.DC\/1705.07478  G. Gopalakrishnan P. D. Hovland C. Iancu S. Krishnamoorthy I. Laguna R. A. Lethin K. Sen S. F. Siegel and A. Solar-Lezama. 2017. Report of the HPC Correctness Summit Jan 25--26 2017 Washington DC. ArXiv e-prints (May 2017). arXiv:cs.DC\/1705.07478","DOI":"10.2172\/1470989"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043174.2043194"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2010.04.201"},{"key":"e_1_3_2_1_18_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2006","unstructured":"Daniel Jackson . 2006 . Software Abstractions: Logic, Language, and Analysis . The MIT Press . Daniel Jackson. 2006. Software Abstractions: Logic, Language, and Analysis. The MIT Press."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908117"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Andreas Kl\u00f6ckner Nicolas Pinto Yunsup Lee Bryan Catanzaro Paul Ivanov and Ahmed Fasih. 2011. PyCUDA and PyOpenCL: A Scripting-Based Approach to GPU Run-Time Code Generation. Parallel Comput. (2011).  Andreas Kl\u00f6ckner Nicolas Pinto Yunsup Lee Bryan Catanzaro Paul Ivanov and Ahmed Fasih. 2011. PyCUDA and PyOpenCL: A Scripting-Based Approach to GPU Run-Time Code Generation. Parallel Comput. (2011).","DOI":"10.1016\/j.parco.2011.09.001"},{"key":"e_1_3_2_1_21_1","volume-title":"Devito: automated fast finite difference computation. CoRR abs\/1608.08658","author":"Kukreja Navjot","year":"2016","unstructured":"Navjot Kukreja , Mathias Louboutin , Felippe Vieira , Fabio Luporini , Michael Lange , and Gerard Gorman . 2016. Devito: automated fast finite difference computation. CoRR abs\/1608.08658 ( 2016 ). http:\/\/arxiv.org\/abs\/1608.08658 Navjot Kukreja, Mathias Louboutin, Felippe Vieira, Fabio Luporini, Michael Lange, and Gerard Gorman. 2016. Devito: automated fast finite difference computation. CoRR abs\/1608.08658 (2016). http:\/\/arxiv.org\/abs\/1608.08658"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/106972.106981"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2145816.2145844"},{"volume-title":"Automated Solution of Differential Equations by the Finite Element Method: The FEniCS Book","author":"Logg Anders","key":"e_1_3_2_1_24_1","unstructured":"Anders Logg , Kent-Andre Mardal , and Garth Wells . 2012. Automated Solution of Differential Equations by the Finite Element Method: The FEniCS Book . Springer Publishing Company, Inc orporated. Anders Logg, Kent-Andre Mardal, and Garth Wells. 2012. Automated Solution of Differential Equations by the Finite Element Method: The FEniCS Book. Springer Publishing Company, Incorporated."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23099-8"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2687415"},{"key":"e_1_3_2_1_27_1","volume-title":"MPI: A Message-Passing Interface Standard, Version 3.1","author":"Interface Forum Message-Passing","year":"2015","unstructured":"Message-Passing Interface Forum . 2015 . MPI: A Message-Passing Interface Standard, Version 3.1 . http:\/\/www.mpi-forum.org\/docs\/docs.html. (4 June 2015). Message-Passing Interface Forum. 2015. MPI: A Message-Passing Interface Standard, Version 3.1. http:\/\/www.mpi-forum.org\/docs\/docs.html. (4 June 2015)."},{"key":"e_1_3_2_1_28_1","volume-title":"SymPy: symbolic computing in Python. Peer J Computer Science 3 (Jan","author":"Meurer Aaron","year":"2017","unstructured":"Aaron Meurer , Christopher P. Smith , Mateusz Paprocki , Ond\u0159ej \u010cert\u00edk , Sergey B. Kirpichev , Matthew Rocklin , AMi T Kumar , Sergiu Ivanov , Jason K. Moore , Sartaj Singh , Thilina Rathnayake , Sean Vig , Brian E. Granger , Richard P. Muller , Francesco Bonazzi , Harsh Gupta , Shivam Vats , Fredrik Johansson , Fabian Pedregosa , Matthew J. Curry , Andy R. Terrel , \u0160t\u011bp\u00e1n Rou\u010dka , Ashutosh Saboo , Isuru Fernando , Sumith Kulal , Robert Cimrman , and Anthony Scopatz . 2017. SymPy: symbolic computing in Python. Peer J Computer Science 3 (Jan . 2017 ), e103. https:\/\/doi.org\/10.7717\/peerj-cs.103 10.7717\/peerj-cs.103 Aaron Meurer, Christopher P. Smith, Mateusz Paprocki, Ond\u0159ej \u010cert\u00edk, Sergey B. Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason K. Moore, Sartaj Singh, Thilina Rathnayake, Sean Vig, Brian E. Granger, Richard P. Muller, Francesco Bonazzi, Harsh Gupta, Shivam Vats, Fredrik Johansson, Fabian Pedregosa, Matthew J. Curry, Andy R. Terrel, \u0160t\u011bp\u00e1n Rou\u010dka, Ashutosh Saboo, Isuru Fernando, Sumith Kulal, Robert Cimrman, and Anthony Scopatz. 2017. SymPy: symbolic computing in Python. Peer J Computer Science 3 (Jan. 2017), e103. https:\/\/doi.org\/10.7717\/peerj-cs.103"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.25080\/shinma-7f4c6e7-00d"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/SC.2016.2"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1365490.1365500"},{"key":"e_1_3_2_1_32_1","unstructured":"OpenMP Architecture Review Board. 2011. OpenMP Application Program Interface Version 3.1. http:\/\/www.openmp.org\/mp-documents\/OpenMP3.1.pdf. (July 2011).  OpenMP Architecture Review Board. 2011. OpenMP Application Program Interface Version 3.1. http:\/\/www.openmp.org\/mp-documents\/OpenMP3.1.pdf. (July 2011)."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_3_2_1_34_1","volume-title":"CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18--22, 2014. Proceedings (Lecture Notes in Computer Science), Armin Biere and Roderick Bloem (Eds.)","volume":"8559","author":"Rakamari\u0107 Zvonimir","year":"2014","unstructured":"Zvonimir Rakamari\u0107 and Michael Emmi . 2014 . SMACK: Decoupling Source Language Details from Verifier Implementations. In Computer Aided Verification - 26th International Conference , CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18--22, 2014. Proceedings (Lecture Notes in Computer Science), Armin Biere and Roderick Bloem (Eds.) , Vol. 8559 . Springer, 106--113. Zvonimir Rakamari\u0107 and Michael Emmi. 2014. SMACK: Decoupling Source Language Details from Verifier Implementations. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18--22, 2014. Proceedings (Lecture Notes in Computer Science), Armin Biere and Roderick Bloem (Eds.), Vol. 8559. Springer, 106--113."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2998441"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2998441"},{"key":"e_1_3_2_1_37_1","first-page":"4","article-title":"Code verification by the method of manufactured solutions","volume":"124","author":"Roache Patrick J","year":"2002","unstructured":"Patrick J Roache . 2002 . Code verification by the method of manufactured solutions . Transactions-American Society of Mechanical Engineers Journal of Fluids Engineering 124 , 1 (2002), 4 -- 10 . Patrick J Roache. 2002. Code verification by the method of manufactured solutions. Transactions-American Society of Mechanical Engineers Journal of Fluids Engineering 124, 1 (2002), 4--10.","journal-title":"Transactions-American Society of Mechanical Engineers Journal of Fluids Engineering"},{"volume-title":"Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations","author":"Schordan Markus","key":"e_1_3_2_1_38_1","unstructured":"Markus Schordan , Pei-Hung Lin , Dan Quinlan , and Louis-No\u00ebl Pouchet . 2014. Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations . Springer Berlin Heidelberg , Berlin, Heidelberg , 493--508. https:\/\/doi.org\/10.1007\/978-3-662-45231-8_41 10.1007\/978-3-662-45231-8_41 Markus Schordan, Pei-Hung Lin, Dan Quinlan, and Louis-No\u00ebl Pouchet. 2014. Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations. Springer Berlin Heidelberg, Berlin, Heidelberg, 493--508. https:\/\/doi.org\/10.1007\/978-3-662-45231-8_41"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1321631.1321746"},{"volume-title":"Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis (SC '15)","author":"Siegel Stephen F.","key":"e_1_3_2_1_40_1","unstructured":"Stephen F. Siegel , Manchun Zheng , Ziqing Luo , Timothy K. Zirkel , Andre V. Marianiello , John G. Edenhofner , Matthew B. Dwyer , and Michael S. Rogers . 2015. CIVL: The Concurrency Intermediate Verification Language . In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis (SC '15) . ACM, New York, Article 61, 12 pages. https:\/\/doi.org\/10.1145\/2807591.2807635 10.1145\/2807591.2807635 Stephen F. Siegel, Manchun Zheng, Ziqing Luo, Timothy K. Zirkel, Andre V. Marianiello, John G. Edenhofner, Matthew B. Dwyer, and Michael S. Rogers. 2015. CIVL: The Concurrency Intermediate Verification Language. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis (SC '15). ACM, New York, Article 61, 12 pages. https:\/\/doi.org\/10.1145\/2807591.2807635"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/3014904.3014906"}],"event":{"name":"SC '17: The International Conference for High Performance Computing, Networking, Storage and Analysis","sponsor":["SIGHPC ACM Special Interest Group on High Performance Computing, Special Interest Group on High Performance Computing","IEEE CS"],"location":"Denver CO USA","acronym":"SC '17"},"container-title":["Proceedings of the First International Workshop on Software Correctness for HPC Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3145344.3145488","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3145344.3145488","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3145344.3145488","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:35Z","timestamp":1750212815000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3145344.3145488"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,12]]},"references-count":41,"alternative-id":["10.1145\/3145344.3145488","10.1145\/3145344"],"URL":"https:\/\/doi.org\/10.1145\/3145344.3145488","relation":{},"subject":[],"published":{"date-parts":[[2017,11,12]]},"assertion":[{"value":"2017-11-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}