{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,10]],"date-time":"2026-09-10T17:06:39Z","timestamp":1789059999355,"version":"build-2803163510"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T00:00:00Z","timestamp":1507766400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2017,10,12]]},"abstract":"<jats:p>Arrays computations are at the core of numerical modelling and computational science applications. However, low-level manipulation of array indices is a source of program error. Many practitioners are aware of the need to ensure program correctness, yet very few of the techniques from the programming research community are applied by scientists. We aim to change that by providing targetted lightweight verification techniques for scientific code. We focus on the all too common mistake of array offset errors as a generalisation of off-by-one errors. Firstly, we report on a code analysis study on eleven real-world computational science code base, identifying common idioms of array usage and their spatial properties. This provides much needed data on array programming idioms common in scientific code. From this data, we designed a lightweight declarative specification language capturing the majority of array access patterns via a small set of combinators. We detail a semantic model, and the design and implementation of a verification tool for our specification language, which both checks and infers specifications. We evaluate our tool on our corpus of scientific code. Using the inference mode, we found roughly 87,000 targets for specification across roughly 1.1 million lines of code, showing that the vast majority of array computations read from arrays in a pattern with a simple, regular, static shape. We also studied the commit logs of one of our corpus packages, finding past bug fixes for which our specification system distinguishes the change and thus could have been applied to detect such bugs.<\/jats:p>","DOI":"10.1145\/3133899","type":"journal-article","created":{"date-parts":[[2017,10,13]],"date-time":"2017-10-13T11:15:45Z","timestamp":1507893345000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Verifying spatial properties of array computations"],"prefix":"10.1145","volume":"1","author":[{"given":"Dominic","family":"Orchard","sequence":"first","affiliation":[{"name":"University of Kent, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mistral","family":"Contrastin","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Danish","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew","family":"Rice","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,10,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPSW.2013.90"},{"key":"e_1_2_2_2_1","volume-title":"MUDPACK: multigrid software for linear elliptic partial differential equations, version 3.0","author":"Adams J.","unstructured":"J. Adams. 1991. MUDPACK: multigrid software for linear elliptic partial differential equations, version 3.0. National Center for Atmospheric Research, Boulder, Colorado. Scientific Computing Division User Doc."},{"key":"e_1_2_2_3_1","volume-title":"Bryan Christopher Catanzaro, Joseph James Gebis, Parry Husbands, Kurt Keutzer, David A. Patterson, William Lester Plishker, John Shalf, Samuel Webb Williams, and Katherine A. Yelick.","author":"Asanovi Krste","year":"2006","unstructured":"Krste Asanovi` c, Ras Bodik, Bryan Christopher Catanzaro, Joseph James Gebis, Parry Husbands, Kurt Keutzer, David A. Patterson, William Lester Plishker, John Shalf, Samuel Webb Williams, and Katherine A. Yelick. 2006. The Landscape of Parallel Computing Research: A View from Berkeley. Technical Report UCB\/EECS-2006-183. EECS Department, University of California, Berkeley. http:\/\/www2.eecs.berkeley.edu\/Pubs\/TechRpts\/2006\/EECS- 2006- 183.html"},{"key":"e_1_2_2_4_1","volume-title":"Special I","author":"Barker Terry","year":"2006","unstructured":"Terry Barker, Haoran Pan, Jonathan Kohler, Rachel Warren, and Sarah Winne. 2006. Decarbonizing the Global Economy with Induced Technological Change: Scenarios to 2100 using E3MG. The Energy Journal 0, Special I (2006), 241\u2013258. https:\/\/ideas.repec.org\/a\/aen\/journl\/2006se- a12.html"},{"key":"e_1_2_2_5_1","volume-title":"ACSL: ANSI C Specification Language.","author":"Baudin Patrick","year":"2008","unstructured":"Patrick Baudin, Jean-Christophe Filli\u00e2tre, Claude March\u00e9, Benjamin Monate, Yannick Moy, and Virgile Prevosto. 2008. ACSL: ANSI C Specification Language. (2008)."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1029\/2001JD000807"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/567806.567807"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.03.013"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/jpdc.1996.0107"},{"key":"e_1_2_2_10_1","volume-title":"ACSL by example, towards a verified C standard library. DEVICESOFT project publication","author":"Burghardt Jochen","year":"2011","unstructured":"Jochen Burghardt, J Gerlach, L Gu, Kerstin Hartig, Hans Pohl, J Soto, and K V\u00f6llinger. 2010. ACSL by example, towards a verified C standard library. DEVICESOFT project publication. Fraunhofer FIRST Institute (December 2011) (2010)."},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the Fourth Workshop on Sustainable Software for Science: Practice and Experiences (WSSSPE4)","volume":"1686","author":"Contrastin Mistral","year":"2016","unstructured":"Mistral Contrastin, Matthew Danish, Dominic Orchard, and Andrew Rice. 2016. Lightning Talk: Supporting Software Sustainability with Lightweight Specifications. In Proceedings of the Fourth Workshop on Sustainable Software for Science: Practice and Experiences (WSSSPE4), University of Manchester, Manchester, UK, September 12\u201314, Vol. 1686. CEUR Workshop Proceedings."},{"key":"e_1_2_2_12_1","volume-title":"CamFort - refactoring, analysis, and verification tool for scientific Fortran programs. https:\/\/camfort.github.com . (2017). Accessed: 23rd","author":"Contrastin Mistral","year":"2017","unstructured":"Mistral Contrastin, Matthew Danish, Dominic Orchard, and Andrew Rice. 2017. CamFort - refactoring, analysis, and verification tool for scientific Fortran programs. https:\/\/camfort.github.com . (2017). Accessed: 23rd August 2017."},{"key":"e_1_2_2_13_1","volume-title":"A survey of edge detection techniques. Computer graphics and image processing 4, 3","author":"Davis Larry S","year":"1975","unstructured":"Larry S Davis. 1975. A survey of edge detection techniques. Computer graphics and image processing 4, 3 (1975), 248\u2013270."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","unstructured":"C. Dawson Q. Du and T. Dupont. 1991. A finite difference domain decomposition algorithm for numerical solution of the heat equation. Math. Comp. 57 195 (1991). 10.1090\/S0025-5718-1991-1079011-4","DOI":"10.1090\/S0025-5718-1991-1079011-4"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5194\/gmdd-3-1587-2010"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1029\/1999GB900085"},{"key":"e_1_2_2_18_1","doi-asserted-by":"crossref","unstructured":"M. Griebel T. Dornsheifer and T. Neunhoeffer. 1997. Numerical simulation in fluid dynamics: a practical introduction. Vol. 3. Society for Industrial Mathematics.","DOI":"10.1137\/1.9780898719703"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908117"},{"key":"e_1_2_2_20_1","volume-title":"https:\/\/github.com\/geodynamics\/specfem3d . (2016). Accessed","author":"Komatitsch Dimitri","year":"2016","unstructured":"Dimitri Komatitsch, Jeroen Tromp, and others. 2016. SPECFEM3D. https:\/\/github.com\/geodynamics\/specfem3d . (2016). Accessed: 15 November 2016."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_5"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","unstructured":"W.L. Oberkampf and C.J. Roy. 2010. Verification and validation in scientific computing. Cambridge University Press. 10.1017\/CBO9780511760396","DOI":"10.1017\/CBO9780511760396"},{"key":"e_1_2_2_23_1","unstructured":"Dominic Orchard Mistral Contrastin Matthew Danish and Andrew Rice. 2017. Proofs for \u2018Verifying Spatial Properties of Array Computations\u2019. Technical Report UCAM-CL-TR-911. University of Cambridge Computer Laboratory 15 JJ Thomson Avenue Cambridge CB3 0FD United Kingdom."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2014.05.064"},{"key":"e_1_2_2_25_1","volume-title":"An introduction to computational physics. (1999)","author":"Pang Tao","unstructured":"Tao Pang. 1999. An introduction to computational physics. (1999). 1st Edition.","edition":"1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","unstructured":"D.E. Post and L.G. Votta. 2005. Computational science demands a new paradigm. Physics today 58 1 (2005) 35\u201341. 10.1063\/1.1881898","DOI":"10.1063\/1.1881898"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462176"},{"key":"e_1_2_2_28_1","volume-title":"Finite-difference approximations to the heat equation. Class Notes","author":"Recktenwald G.W.","year":"2004","unstructured":"G.W. Recktenwald. 2004. Finite-difference approximations to the heat equation. Class Notes (2004). http:\/\/www.f.kth.se\/ ~jjalap\/numme\/FDheat.pdf ."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250754"},{"key":"e_1_2_2_30_1","unstructured":"David Sorenson Richard Lehoucq Chao Yang Kristi Maschhoff Sylvestre Ledru and Allan Cornet. 2017. ARPACK-NG. https:\/\/github.com\/opencollab\/arpack- ng . (2017)."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1989493.1989508"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00024-014-0825-8"},{"key":"e_1_2_2_33_1","volume-title":"IFIP TC","volume":"2","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler. 1990. Linear types can change the world. In IFIP TC, Vol. 2. Citeseer, 347\u2013359."},{"key":"e_1_2_2_34_1","doi-asserted-by":"crossref","unstructured":"David A Wheeler. 2001. SLOCCount. (2001).","DOI":"10.1515\/semi.2001.009"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1002\/qj.49712555707"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133899","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3133899","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,10]],"date-time":"2026-09-10T16:11:39Z","timestamp":1789056699000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3133899"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,12]]},"references-count":35,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2017,10,12]]}},"alternative-id":["10.1145\/3133899"],"URL":"https:\/\/doi.org\/10.1145\/3133899","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10,12]]},"assertion":[{"value":"2017-10-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}