{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:52:54Z","timestamp":1742914374489,"version":"3.40.3"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319178219"},{"type":"electronic","value":"9783319178226"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17822-6_1","type":"book-chapter","created":{"date-parts":[[2015,4,22]],"date-time":"2015-04-22T05:57:31Z","timestamp":1429682251000},"page":"3-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Analyzing Array Manipulating Programs by Program Transformation"],"prefix":"10.1007","author":[{"given":"J. Robert M.","family":"Cornish","sequence":"first","affiliation":[]},{"given":"Graeme","family":"Gange","sequence":"additional","affiliation":[]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schachte","sequence":"additional","affiliation":[]},{"given":"Harald","family":"S\u00f8ndergaard","sequence":"additional","affiliation":[]},{"given":"Peter J.","family":"Stuckey","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,23]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-28717-6_7","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Alberti","year":"2012","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 46\u201361. Springer, Heidelberg (2012)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.\u00c6., Schmidt, D.A., Sudborough, I. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85\u2013108. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-36377-7_5"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-319-10431-7_20","volume-title":"Software Engineering and Formal Methods","author":"G Brat","year":"2014","unstructured":"Brat, G., Navas, J.A., Shi, N., Venet, A.: IKOS: a framework for static analysis based on abstract interpretation. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 271\u2013277. Springer, Heidelberg (2014)"},{"key":"1_CR4","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: POPL 1977, pp. 238\u2013252. ACM Press (1977)","DOI":"10.1145\/512950.512973"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL 2011, pp. 105\u2013118. ACM Press (2011)","DOI":"10.1145\/1925844.1926399"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-54013-4_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E De Angelis","year":"2014","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verifying array programs by transforming verification conditions. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 182\u2013202. Springer, Heidelberg (2014)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"issue":"1\u20133","key":"1_CR8","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: POPL 2005, pp. 338\u2013350. ACM Press (2005)","DOI":"10.1145\/1047659.1040333"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL 2008, pp. 235\u2013246. ACM Press (2008)","DOI":"10.1145\/1328897.1328468"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: PLDI 2008, pp. 339\u2013348. ACM Press (2008)","DOI":"10.1145\/1379022.1375623"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-35873-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Larraz","year":"2013","unstructured":"Larraz, D., Rodr\u00edguez-Carbonell, E., Rubio, A.: SMT-based array invariant generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 169\u2013188. Springer, Heidelberg (2013)"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Nguyen, T.V., Kapur, D., Weimer, W., Forrest, S.: Using dynamic analysis to discover polynomial and array invariants. In: Proceedings of the 34th International Conference on Software Engineering, pp. 760\u2013770. IEEE (2012)","DOI":"10.1109\/ICSE.2012.6227149"},{"key":"1_CR16","unstructured":"P\u00e9ron, M.: Contributions \u00e0 l\u2019analyse statique de programmes manipulant des tableaux. Ph.D. thesis, Universit\u00e9 de Grenoble (2010)"},{"key":"1_CR17","unstructured":"Regehr, J.: Uninitialized variables. Web blog, http:\/\/blog.regehr.org\/archives\/519, Accessed 18 June 2014"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17822-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,24]],"date-time":"2023-01-24T11:24:41Z","timestamp":1674559481000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17822-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319178219","9783319178226"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17822-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"23 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}