{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T08:26:37Z","timestamp":1746001597941},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662534120"},{"type":"electronic","value":"9783662534137"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-53413-7_13","type":"book-chapter","created":{"date-parts":[[2016,8,30]],"date-time":"2016-08-30T07:57:11Z","timestamp":1472543831000},"page":"257-277","source":"Crossref","is-referenced-by-count":2,"title":["Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Programs"],"prefix":"10.1007","author":[{"given":"Matthieu","family":"Journault","sequence":"first","affiliation":[]},{"given":"Antoine","family":"Min\u00e9","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,31]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/978-3-540-78739-6_14","volume-title":"Programming Languages and Systems","author":"X Allamigeon","year":"2008","unstructured":"Allamigeon, X.: Non-disjunctive numerical domain for array predicate abstraction. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 163\u2013177. Springer, Heidelberg (2008)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/11823230_4","volume-title":"Static Analysis","author":"X Allamigeon","year":"2006","unstructured":"Allamigeon, X., Godard, W., Hymans, C.: Static analysis of string manipulations in critical embedded C programs. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 35\u201351. Springer, Heidelberg (2006)"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proceedings of PLDI 2003, pp. 196\u2013207. ACM, June 2003","DOI":"10.1145\/780822.781153"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/978-3-540-78791-4_9","volume-title":"Compiler Construction","author":"U Bondhugula","year":"2008","unstructured":"Bondhugula, U., Baskaran, M., Krishnamoorthy, S., Ramanujam, J., Rountev, A., Sadayappan, P.: Automatic transformations for communication-minimized parallelization and locality optimization in the polyhedral model. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 132\u2013146. Springer, Heidelberg (2008)"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Bondhugula, U., Hartono, A., Ramanujam, J., Sadayappan, P.: A practical automatic polyhedral parallelizer and locality optimizer. In: Proceedings of PLDI 2008, pp. 101\u2013113. ACM (2008)","DOI":"10.1145\/1375581.1375595"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","first-page":"243","volume-title":"Verification: Theory and Practice","author":"P Cousot","year":"2004","unstructured":"Cousot, P.: Verification by abstract interpretation. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 243\u2013268. Springer, Heidelberg (2004)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Proceedings of POPL 2011, pp. 105\u2013118. ACM (2011)","DOI":"10.1145\/1926385.1926399"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of POPL 1978, pp. 84\u201396. ACM (1978)","DOI":"10.1145\/512760.512770"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/978-3-642-11957-6_14","volume-title":"Programming Languages and Systems","author":"I Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 246\u2013266. Springer, Heidelberg (2010)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/978-3-540-24730-2_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Gopan","year":"2004","unstructured":"Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 512\u2013529. Springer, Heidelberg (2004)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: Proceedings of POPL 2005, pp. 338\u2013350. ACM (2005)","DOI":"10.1145\/1047659.1040333"},{"issue":"6","key":"13_CR13","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1145\/1379022.1375623","volume":"43","author":"N Halbwachs","year":"2008","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. SIGPLAN Not. 43(6), 339\u2013348 (2008)","journal-title":"SIGPLAN Not."},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proceedings of POPL 2006, pp. 42\u201354. ACM (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1007\/11942634","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348\u2013363. Springer, Heidelberg (2006)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/978-3-662-48288-9_13","volume-title":"Static Analysis","author":"D Monniaux","year":"2015","unstructured":"Monniaux, D., Alberti, F.: A simple abstraction of arrays and maps by program translation. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 217\u2013234. Springer, Heidelberg (2015)"},{"issue":"5","key":"13_CR17","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/1275497.1275501","volume":"29","author":"X Rival","year":"2007","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5), 26 (2007)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/3-540-61739-6_53","volume-title":"Static Analysis","author":"A Venet","year":"1996","unstructured":"Venet, A.: Abstract cofibered domains: application to the alias analysis of untyped programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 366\u2013382. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-53413-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T17:38:34Z","timestamp":1498325914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-53413-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662534120","9783662534137"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-53413-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}