{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:24:53Z","timestamp":1740122693635,"version":"3.37.3"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,2,12]],"date-time":"2018-02-12T00:00:00Z","timestamp":1518393600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["681393"],"award-info":[{"award-number":["681393"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1007\/s10703-017-0311-x","type":"journal-article","created":{"date-parts":[[2018,2,12]],"date-time":"2018-02-12T05:56:44Z","timestamp":1518415004000},"page":"221-258","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Inferring functional properties of matrix manipulating programs by abstract interpretation"],"prefix":"10.1007","volume":"53","author":[{"given":"Matthieu","family":"Journault","sequence":"first","affiliation":[]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,2,12]]},"reference":[{"key":"311_CR1","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the POPL 1977. ACM, pp 238\u2013252","DOI":"10.1145\/512950.512973"},{"key":"311_CR2","doi-asserted-by":"crossref","unstructured":"Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Min\u00e9 A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: Proceedings of the PLDI\u201903. ACM, pp 196\u2013207","DOI":"10.1145\/781131.781153"},{"key":"311_CR3","doi-asserted-by":"crossref","unstructured":"Allamigeon X (2008) Non-disjunctive numerical domain for array predicate abstraction. In: SOP 2008, volume 4960 of LNCS. Springer, pp 163\u2013177","DOI":"10.1007\/978-3-540-78739-6_14"},{"key":"311_CR4","doi-asserted-by":"crossref","unstructured":"Cousot P (2003) Verification by abstract interpretation. In: Verification: theory and practice, essays dedicated to Zohar Manna on the occasion of his 64th birthday, volume 2772 of LNCS. Springer, pp 243\u2013268","DOI":"10.1007\/978-3-540-39910-0_11"},{"key":"311_CR5","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R, Logozzo F (2011) A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of POPL 2011. ACM, pp 105\u2013118","DOI":"10.1145\/1926385.1926399"},{"key":"311_CR6","doi-asserted-by":"crossref","unstructured":"Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Proceeings of POPL 1978. ACM, pp 84\u201396","DOI":"10.1145\/512760.512770"},{"key":"311_CR7","doi-asserted-by":"crossref","unstructured":"Bondhugula U, Baskaran M, Krishnamoorthy S, Ramanujam J, Rountev A, Sadayappan P (2008) Automatic transformations for communication-minimized parallelization and locality optimization in the polyhedral model. In: CC 2008, volume 4959 of LNCS. Springer, pp 132\u2013146","DOI":"10.1007\/978-3-540-78791-4_9"},{"key":"311_CR8","doi-asserted-by":"crossref","unstructured":"Bondhugula U, Hartono A, Ramanujam J, Sadayappan P (2008) A practical automatic polyhedral parallelizer and locality optimizer. In: Proceedings of the PLDI 2008. ACM, pp 101\u2013113","DOI":"10.1145\/1375581.1375595"},{"key":"311_CR9","doi-asserted-by":"crossref","unstructured":"Leroy X (2006) Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proceedings of the POPL 2006. ACM, pp 42\u201354","DOI":"10.1145\/1111037.1111042"},{"key":"311_CR10","doi-asserted-by":"crossref","unstructured":"Journault M, Min\u00e9 A (2016) Static analysis by abstract interpretation of the functional correctness of matrix manipulating programs. In Xavier R (eds) Static analysis\u201423rd international symposium, SAS 2016, Edinburgh, UK, September 8\u201310, 2016, proceedings, volume 9837 of lecture notes in computer science. Springer, pp 257\u2013277","DOI":"10.1007\/978-3-662-53413-7_13"},{"key":"311_CR11","doi-asserted-by":"crossref","unstructured":"Venet A (1996) Abstract cofibered domains: application to the alias analysis of untyped programs. In: SAS\u201996, volume 1145 of LNCS. Springer, pp 366\u2013382","DOI":"10.1007\/3-540-61739-6_53"},{"issue":"5","key":"311_CR12","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X Rival","year":"2007","unstructured":"Rival X, Mauborgne L (2007) The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5):26","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"311_CR13","doi-asserted-by":"crossref","unstructured":"Cousot P, Cousot R (2002) Modular static program analysis. In: Horspool RN (ed) Compiler construction, 11th international conference, CC 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8\u201312, 2002, proceedings, volume 2304 of lecture notes in computer science. Springer, pp 159\u2013178","DOI":"10.1007\/3-540-45937-5_13"},{"key":"311_CR14","unstructured":"Min\u00e9 A (2006) Symbolic methods to enhance the precision of numerical abstract domains. In: VMCAI 2006, volume 3855 of LNCS. Springer, pp 348\u2013363"},{"key":"311_CR15","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A (2006) The octagon abstract domain. Higher Order Symb Comput (HOSC) 19(1):31\u2013100 http:\/\/www-apr.lip6.fr\/~mine\/publi\/article-mine-HOSC06.pdf","DOI":"10.1007\/s10990-006-8609-1"},{"key":"311_CR16","doi-asserted-by":"crossref","unstructured":"Gopan D, DiMaio F, Dor N, Reps T, Sagiv M (2004) Numeric domains with summarized dimensions. In: TACAS 2004. Springer, pp 512\u2013529","DOI":"10.1007\/978-3-540-24730-2_38"},{"key":"311_CR17","doi-asserted-by":"crossref","unstructured":"Gopan D, Reps TW, Sagiv S (2005) A framework for numeric analysis of array operations. In: Proceedings of POPL 2005. ACM, pp 338\u2013350","DOI":"10.1145\/1040305.1040333"},{"issue":"6","key":"311_CR18","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1145\/1379022.1375623","volume":"43","author":"N Halbwachs","year":"2008","unstructured":"Halbwachs N, P\u00e9ron M (2008) Discovering properties about arrays in simple programs. SIGPLAN Not 43(6):339\u2013348","journal-title":"SIGPLAN Not"},{"key":"311_CR19","doi-asserted-by":"crossref","unstructured":"Allamigeon X, Godard W, Hymans C (2006) Static analysis of string manipulations in critical embedded C programs. In: SAS 2006. Springer, pp 35\u201351","DOI":"10.1007\/11823230_4"},{"key":"311_CR20","doi-asserted-by":"crossref","unstructured":"Dillig I, Dillig T, Aiken A (2010) Fluid updates: beyond strong vs. weak updates. In: ESOP 2010. Springer, pp 246\u2013266","DOI":"10.1007\/978-3-642-11957-6_14"},{"key":"311_CR21","doi-asserted-by":"crossref","unstructured":"Monniaux D, Alberti F (2015) A simple abstraction of arrays and maps by program translation. In: SAS 2015, volume 9291 of LNCS. Springer, pp 217\u2013234","DOI":"10.1007\/978-3-662-48288-9_13"},{"key":"311_CR22","unstructured":"Peng Y. Automate convergence rate proof for gradient descent on quadratic functions"},{"issue":"4","key":"311_CR23","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1145\/504210.504213","volume":"27","author":"JA Gunnels","year":"2001","unstructured":"Gunnels JA, Gustavson FG, Henry G, van de Geijn RA (2001) FLAME: formal linear algebra methods environment. ACM Trans. Math. Softw. 27(4):422\u2013455","journal-title":"ACM Trans. Math. Softw."},{"key":"311_CR24","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Hottelier T, Kov\u00e1cs L, Voronkov A (2010) Invariant and type inference for matrices. In: Barthe G, Hermenegildo MV (eds) Verification, model checking, and abstract interpretation, 11th international conference, VMCAI 2010, Madrid, Spain, January 17\u201319, 2010, proceedings, volume 5944 of lecture notes in computer science. Springer, pp 163\u2013179","DOI":"10.1007\/978-3-642-11319-2_14"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-017-0311-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0311-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-017-0311-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T16:29:52Z","timestamp":1570724992000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-017-0311-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,2,12]]},"references-count":24,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["311"],"URL":"https:\/\/doi.org\/10.1007\/s10703-017-0311-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2018,2,12]]},"assertion":[{"value":"12 February 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}