{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T15:14:35Z","timestamp":1784560475432,"version":"3.55.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319899596","type":"print"},{"value":"9783319899602","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89960-2_12","type":"book-chapter","created":{"date-parts":[[2018,4,11]],"date-time":"2018-04-11T10:14:43Z","timestamp":1523441683000},"page":"213-231","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Property Checking Array Programs Using Loop Shrinking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7999-4727","authenticated-orcid":false,"given":"Shrawan","family":"Kumar","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amitabha","family":"Sanyal","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"R.","family":"Venkatesh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Punit","family":"Shah","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,4,12]]},"reference":[{"issue":"4","key":"12_CR1","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1145\/29873.29875","volume":"9","author":"R Allen","year":"1987","unstructured":"Allen, R., Kennedy, K.: Automatic translation of fortran programs to vector form. ACM Trans. Program. Lang. Syst. 9(4), 491\u2013542 (1987)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR2","unstructured":"Beyer, D.: SV-COMP 2017\u20136th International Conference on Software Verification (2017). \n                      https:\/\/sv-comp.sosy-lab.org"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation","author":"B Blanchet","year":"2002","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.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85\u2013108. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-36377-7_5"},{"issue":"5","key":"12_CR5","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/780822.781153","volume":"38","author":"Bruno Blanchet","year":"2003","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 the PLDI 2003, pp. 196\u2013207. ACM, New York (2003)","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Carter, M., He, S., Whitaker, J., Rakamari\u0107, Z., Emmi, M.: Smack software verification toolchain. In: Proceedings of the 38th International Conference on Software Engineering Companion, ICSE 2016, pp. 589\u2013592. ACM, New York (2016)","DOI":"10.1145\/2889160.2889163"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-662-54580-5_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Chimdyalwar","year":"2017","unstructured":"Chimdyalwar, B., Darke, P., Chauhan, A., Shah, P., Kumar, S., Venkatesh, R.: VeriAbs: verification by abstraction (competition contribution). In: Legay, A., Margaria, T. (eds.) TACAS 2017, Part II. LNCS, vol. 10206, pp. 404\u2013408. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54580-5_32"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). \n                      https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1007\/978-3-540-31980-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2005","unstructured":"Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstraction for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 570\u2013574. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/978-3-540-31980-1_40"},{"key":"12_CR10","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: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252. ACM, New York (1977)","DOI":"10.1145\/512950.512973"},{"issue":"1","key":"12_CR11","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/1925844.1926399","volume":"46","author":"Patrick Cousot","year":"2011","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: SIGPLAN Not, vol. 46, no. 1, pp. 105\u2013118, January 2011","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Darke, P., Chimdyalwar, B., Venkatesh, R., Shrotri, U., Metta, R.: Over-approximating loops to prove properties using bounded model checking. In: Proceedings of the DATE 2015, pp. 1407\u20131412. EDA Consortium, San Jose (2015)","DOI":"10.7873\/DATE.2015.0245"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"12_CR14","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-11957-6_14"},{"issue":"1","key":"12_CR15","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/565816.503291","volume":"37","author":"Cormac Flanagan","year":"2002","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings of the POPL 2002, pp. 191\u2013202. ACM, New York (2002)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"12_CR16","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/1047659.1040333","volume":"40","author":"Denis Gopan","year":"2005","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: SIGPLAN Not. vol. 40, no. 1, pp. 338\u2013350, January 2005","journal-title":"ACM SIGPLAN Notices"},{"issue":"6","key":"12_CR17","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1145\/1379022.1375623","volume":"43","author":"Nicolas Halbwachs","year":"2008","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: SIGPLAN Not, vol. 43, no. 6, pp. 339\u2013348, June 2008","journal-title":"ACM SIGPLAN Notices"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-63139-4_16","volume-title":"Logic-Based Program Synthesis and Transformation","author":"A Jana","year":"2017","unstructured":"Jana, A., Khedker, U.P., Datar, A., Venkatesh, R., Niyas, C.: Scaling bounded model checking by transforming programs with arrays. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 275\u2013292. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63139-4_16"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: Proceedings of POPL 2014, pp. 529\u2013540. ACM, New York (2014)","DOI":"10.1145\/2535838.2535843"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-73368-3_23","volume-title":"Computer Aided Verification","author":"R Jhala","year":"2007","unstructured":"Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193\u2013206. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-73368-3_23"},{"key":"12_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-31980-1_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KL McMillan","year":"2005","unstructured":"McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1\u201312. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/978-3-540-31980-1_1"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). \n                      https:\/\/doi.org\/10.1007\/978-3-662-48288-9_13"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-662-53413-7_18","volume-title":"Static Analysis","author":"D Monniaux","year":"2016","unstructured":"Monniaux, D., Gonnord, L.: Cell morphing: from array programs to array-free Horn clauses. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 361\u2013382. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-53413-7_18"},{"key":"12_CR24","unstructured":"Wang, D.: Tool ceagle (2017). \n                      http:\/\/sts.thss.tsinghua.edu.cn\/ceagle"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89960-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T03:14:36Z","timestamp":1583205276000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89960-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899596","9783319899602"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89960-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"12 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}