{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T18:16:39Z","timestamp":1725905799096},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319631387"},{"type":"electronic","value":"9783319631394"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-63139-4_16","type":"book-chapter","created":{"date-parts":[[2017,7,24]],"date-time":"2017-07-24T03:22:55Z","timestamp":1500866575000},"page":"275-292","source":"Crossref","is-referenced-by-count":6,"title":["Scaling Bounded Model Checking by Transforming Programs with Arrays"],"prefix":"10.1007","author":[{"given":"Anushri","family":"Jana","sequence":"first","affiliation":[]},{"given":"Uday P.","family":"Khedker","sequence":"additional","affiliation":[]},{"given":"Advaita","family":"Datar","sequence":"additional","affiliation":[]},{"given":"R.","family":"Venkatesh","sequence":"additional","affiliation":[]},{"given":"Niyas","family":"C.","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,25]]},"reference":[{"unstructured":"2015 4th International Competition on Software Verification. http:\/\/sv-comp.sosy-lab.org\/2015\/results\/ . Accessed 12 Feb 2017","key":"16_CR1"},{"unstructured":"2016 5th International Competition on Software Verification. http:\/\/sv-comp.sosy-lab.org\/2016\/results\/results-verified\/ . Accessed 12 Feb 2017","key":"16_CR2"},{"doi-asserted-by":"crossref","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. In: Formal Methods in System Design (2014)","key":"16_CR3","DOI":"10.1007\/s10703-014-0209-9"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-319-11936-6_2","volume-title":"Automated Technology for Verification and Analysis","author":"F Alberti","year":"2014","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Booster: an acceleration-based verification framework for array programs. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 18\u201323. Springer, Cham (2014). doi: 10.1007\/978-3-319-11936-6_2"},{"doi-asserted-by":"crossref","unstructured":"Alberti, F., Monniaux, D.: Polyhedra to the rescue of array interpolants. In: Annual ACM Symposium on Applied Computing (2015)","key":"16_CR5","DOI":"10.1145\/2695664.2695784"},{"doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The slam project: debugging system software via static analysis. In: ACM SIGPLAN Notices, vol. 37 (2002)","key":"16_CR6","DOI":"10.1145\/503272.503274"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-540-69738-1_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Invariant synthesis for combined theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 378\u2013394. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-69738-1_27"},{"key":"16_CR8","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). doi: 10.1007\/3-540-36377-7_5"},{"unstructured":"CBMC. http:\/\/www.cprover.org\/cbmc\/ . Accessed 12 Feb 2017","key":"16_CR9"},{"doi-asserted-by":"crossref","unstructured":"Chimdyalwar, B., Kumar, S.: Effective false positive filtering for evolving software. In: ISEC (2011)","key":"16_CR10","DOI":"10.1145\/1953355.1953369"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Computer Aided Verification","author":"F Copty","year":"2001","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 436\u2013453. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44585-4_43"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-17822-6_1","volume-title":"Logic-Based Program Synthesis and Transformation","author":"JRM Cornish","year":"2015","unstructured":"Cornish, J.R.M., Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: Analyzing array manipulating programs by program transformation. In: Proietti, M., Seki, H. (eds.) LOPSTR 2014. LNCS, vol. 8981, pp. 3\u201320. Springer, Cham (2015). doi: 10.1007\/978-3-319-17822-6_1"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: ACM SIGPLAN Notices, vol. 46 (2011)","key":"16_CR13","DOI":"10.1145\/1926385.1926399"},{"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: DATE (2015)","key":"16_CR14","DOI":"10.7873\/DATE.2015.0245"},{"key":"16_CR15","doi-asserted-by":"crossref","first-page":"329","DOI":"10.3233\/FI-2015-1257","volume":"140","author":"E Angelis De","year":"2015","unstructured":"De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: A rule-based verification strategy for array manipulating programs. Fundamenta Informaticae 140, 329\u2013355 (2015)","journal-title":"Fundamenta Informaticae"},{"key":"16_CR16","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). doi: 10.1007\/978-3-642-11957-6_14"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-642-18070-5_2","volume-title":"Formal Verification of Object-Oriented Software","author":"M F\u00e4hndrich","year":"2011","unstructured":"F\u00e4hndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10\u201330. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-18070-5_2"},{"key":"16_CR18","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/565816.503291","volume":"37","author":"C Flanagan","year":"2002","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. ACM SIGPLAN Not. 37, 191\u2013202 (2002)","journal-title":"ACM SIGPLAN Not."},{"issue":"1","key":"16_CR19","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1145\/1047659.1040333","volume":"40","author":"D Gopan","year":"2005","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. ACM SIGPLAN Not. 40(1), 338\u2013350 (2005)","journal-title":"ACM SIGPLAN Not."},{"doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: POPL (2008)","key":"16_CR20","DOI":"10.1145\/1328438.1328468"},{"key":"16_CR21","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. ACM SIGPLAN Not. 43, 339\u2013348 (2008)","journal-title":"ACM SIGPLAN Not."},{"key":"16_CR22","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/77606.77608","volume":"12","author":"S Horwitz","year":"1990","unstructured":"Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. ACM Trans. Program. Lang. Syst. 12, 26\u201360 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"unstructured":"Ice Cast. http:\/\/icecast.org\/ . Accessed 12 Feb 2017","key":"16_CR23"},{"doi-asserted-by":"crossref","unstructured":"Jana, A., Khedker, U.P., Datar, A., Venkatesh, R.: Scaling bounded model checking by transforming programs with arrays. CoRR, arXiv:1606.06974 (2016)","key":"16_CR24","DOI":"10.1007\/978-3-319-63139-4_16"},{"doi-asserted-by":"crossref","unstructured":"Khare, S., Saraswat, S., Kumar, S.: Static program analysis of large embedded code base: an experience. In: ISEC (2011)","key":"16_CR25","DOI":"10.1145\/1953355.1953368"},{"key":"16_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-39799-8_26","volume-title":"Computer Aided Verification","author":"D Kroening","year":"2013","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 381\u2013396. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_26"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/978-3-662-46081-8_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Liu","year":"2015","unstructured":"Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 282\u2013299. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-46081-8_16"},{"key":"16_CR28","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). doi: 10.1007\/978-3-662-53413-7_18"},{"unstructured":"SV-COMP 2016 Benchmarks. https:\/\/sv-comp.sosy-lab.org\/2016\/benchmarks.php . Accessed 12 Feb 2017","key":"16_CR29"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63139-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T12:34:16Z","timestamp":1569933256000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63139-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319631387","9783319631394"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63139-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}