{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T04:23:03Z","timestamp":1751430183687,"version":"3.41.0"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,2,14]],"date-time":"2018-02-14T00:00:00Z","timestamp":1518566400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,2,14]],"date-time":"2018-02-14T00:00:00Z","timestamp":1518566400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"U.S. Department of Energy, Office of Science, Advanced Scientific Computing Research Program","award":["DE-SC0008923"],"award-info":[{"award-number":["DE-SC0008923"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1253229"],"award-info":[{"award-number":["CCF-1253229"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s10817-018-9451-y","type":"journal-article","created":{"date-parts":[[2018,2,14]],"date-time":"2018-02-14T06:17:04Z","timestamp":1518589024000},"page":"193-213","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms"],"prefix":"10.1007","volume":"62","author":[{"given":"Thomas","family":"Gr\u00e9goire","sequence":"first","affiliation":[]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,2,14]]},"reference":[{"key":"9451_CR1","doi-asserted-by":"crossref","unstructured":"Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, pp. 113\u2013132. ACM (2012)","DOI":"10.1145\/2398857.2384625"},{"key":"9451_CR2","doi-asserted-by":"crossref","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.C., Mayero, M., Melquiond, G., Weis, P.: Formal proof of a wave equation resolution scheme: the method error. In: Interactive Theorem Proving, pp. 147\u2013162. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_12"},{"issue":"4","key":"9451_CR3","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/s10817-012-9255-4","volume":"50","author":"S Boldo","year":"2013","unstructured":"Boldo, S., Cl\u00e9ment, F., Filli\u00e2tre, J.C., Mayero, M., Melquiond, G., Weis, P.: Wave equation numerical resolution: a comprehensive mechanized proof of a C program. J. Autom. Reason. 50(4), 423\u2013456 (2013)","journal-title":"J. Autom. Reason."},{"key":"9451_CR4","doi-asserted-by":"crossref","unstructured":"Cachera, D., Pichardie, D.: Embedding of systems of affine recurrence equations in Coq. In: TPHOLs, pp. 155\u2013170. Springer (2003)","DOI":"10.1007\/10930755_10"},{"key":"9451_CR5","volume-title":"An Introduction to Numerical Methods and Analysis","author":"JF Epperson","year":"2014","unstructured":"Epperson, J.F.: An Introduction to Numerical Methods and Analysis. Wiley, Hoboken (2014)"},{"key":"9451_CR6","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-61736-1_44","volume-title":"The Data Parallel Programming Model","author":"P Feautrier","year":"1996","unstructured":"Feautrier, P.: Automatic parallelization in the polytope model. In: Perrin, G.-R., Darte, A. (eds.) The Data Parallel Programming Model, pp. 79\u2013103. Springer, Berlin (1996)"},{"key":"9451_CR7","doi-asserted-by":"crossref","unstructured":"Frigo, M., Strumpen, V.: Cache oblivious stencil computations. In: Proceedings of the 19th Annual International Conference on Supercomputing, pp. 361\u2013366. ACM (2005)","DOI":"10.1145\/1088149.1088197"},{"issue":"2","key":"9451_CR8","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/s00224-007-9098-2","volume":"45","author":"M Frigo","year":"2009","unstructured":"Frigo, M., Strumpen, V.: The cache complexity of multithreaded cache oblivious algorithms. Theory Comput. Syst. 45(2), 203\u2013233 (2009)","journal-title":"Theory Comput. Syst."},{"issue":"4","key":"9451_CR9","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1038\/scientificamerican1070-120","volume":"223","author":"M Gardner","year":"1970","unstructured":"Gardner, M.: Mathematical games\u2014the fantastic combinations of John Conway\u2019s new solitaire game \u201cLife\u201d. Sci. Am. 223(4), 120\u2013123 (1970)","journal-title":"Sci. Am."},{"key":"9451_CR10","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, T., Chlipala, A.: Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms. In: International Conference on Interactive Theorem Proving, pp. 167\u2013183. Springer (2016)","DOI":"10.1007\/978-3-319-43144-4_11"},{"key":"9451_CR11","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-32347-8_26","volume-title":"Interactive Theorem Proving","author":"F Immler","year":"2012","unstructured":"Immler, F., H\u00f6lzl, J.: Numerical analysis of ordinary differential equations in Isabelle\/HOL. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving, pp. 377\u2013392. Springer, Berlin (2012)"},{"key":"9451_CR12","doi-asserted-by":"crossref","unstructured":"Kelly, W., Pugh, W.: Unifying framework for iteration reordering transformations. In: Proceedings of IEEE First International Conference on Algorithms and Architectures for Parallel Processing, vol.\u00a01, pp. 153\u2013162 (1995)","DOI":"10.1109\/ICAPP.1995.472180"},{"key":"9451_CR13","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898717839","volume-title":"Finite Difference Methods for Ordinary and Partial Differential Equations: Steady-State and Time-Dependent Problems","author":"RJ LeVeque","year":"2007","unstructured":"LeVeque, R.J.: Finite Difference Methods for Ordinary and Partial Differential Equations: Steady-State and Time-Dependent Problems, vol. 98. SIAM, Philadelphia (2007)"},{"key":"9451_CR14","doi-asserted-by":"crossref","unstructured":"Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 187\u2013196. ACM (2010)","DOI":"10.1145\/1882291.1882320"},{"key":"9451_CR15","doi-asserted-by":"crossref","unstructured":"Li, G., Li, P., Sawaya, G., Gopalakrishnan, G., Ghosh, I., Rajan, S.P.: GKLEE: concolic verification and test generation for GPUs. In: PPOPP, pp. 215\u2013224 (2012)","DOI":"10.1145\/2370036.2145844"},{"key":"9451_CR16","unstructured":"Loechner, V.: PolyLib: A library for manipulating parameterized polyhedra. http:\/\/camlunity.ru\/swap\/Library\/Conflux\/Techniques%20-%20Code%20Analysis%20and%20Transformations%20(Polyhedral)\/Free%20Libraries\/polylib.ps . Accessed 10 Feb 2018."},{"key":"9451_CR17","doi-asserted-by":"crossref","unstructured":"Maydan, D., Hennessy, J., Lam, M.: Efficient and exact data dependence analysis. In: Proceedings of the ACM SIGPLAN\u201991 Conference on Programming Language Design and Implementation (1991)","DOI":"10.1145\/113445.113447"},{"key":"9451_CR18","doi-asserted-by":"crossref","unstructured":"Orchard, D., Mycroft, A.: Efficient and correct stencil computation via pattern matching and static typing. arXiv preprint: arXiv:1109.0777 (2011)","DOI":"10.4204\/EPTCS.66.4"},{"key":"9451_CR19","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM\/IEEE Conference on Supercomputing, pp. 4\u201313. ACM (1991)","DOI":"10.1145\/125826.125848"},{"key":"9451_CR20","doi-asserted-by":"crossref","unstructured":"Solar-Lezama, A., Arnold, G., Tancau, L., Bodik, R., Saraswat, V., Seshia, S.: Sketching stencils. In: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 167\u2013178. ACM (2007)","DOI":"10.1145\/1273442.1250754"},{"key":"9451_CR21","doi-asserted-by":"crossref","unstructured":"Tang, Y., Chowdhury, R.A., Kuszmaul, B.C., Luk, C.K., Leiserson, C.E.: The Pochoir stencil compiler. In: Proceedings of the Twenty-Third Annual ACM Symposium on Parallelism in Algorithms and Architectures, pp. 117\u2013128. ACM (2011)","DOI":"10.1145\/1989493.1989508"},{"issue":"8","key":"9451_CR22","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1145\/79173.79181","volume":"33","author":"LG Valiant","year":"1990","unstructured":"Valiant, L.G.: A bridging model for parallel computation. Commun. ACM 33(8), 103\u2013111 (1990)","journal-title":"Commun. ACM"},{"key":"9451_CR23","doi-asserted-by":"crossref","unstructured":"Xu, Z., Kamil, S., Solar-Lezama, A.: MSL: a synthesis enabled language for distributed implementations. In: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, pp. 311\u2013322. IEEE Press (2014)","DOI":"10.1109\/SC.2014.31"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9451-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9451-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9451-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T20:35:45Z","timestamp":1751402145000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9451-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,14]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["9451"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9451-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,2,14]]},"assertion":[{"value":"7 February 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 January 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 February 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}