{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T14:13:54Z","timestamp":1743084834436,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031562211"},{"type":"electronic","value":"9783031562228"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-56222-8_12","type":"book-chapter","created":{"date-parts":[[2024,3,19]],"date-time":"2024-03-19T08:02:30Z","timestamp":1710835350000},"page":"206-224","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Template-Based Verification of\u00a0Array-Manipulating Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0608-0748","authenticated-orcid":false,"given":"Viktor","family":"Mal\u00edk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5713-1381","authenticated-orcid":false,"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2746-8792","authenticated-orcid":false,"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,3,20]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Afzal, M., et al.: VeriAbs: verification by abstraction and test generation. In: Proceedings of the 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 1138\u20131141 (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00121","DOI":"10.1109\/ASE.2019.00121"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Bouajjani, A., Esparza, J.: Model checking procedural programs. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 541\u2013572. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_17","DOI":"10.1007\/978-3-319-10575-8_17"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: an overview. In: Proceedings of the 2004 International Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, pp. 49\u201369. CASSIS 2004, Springer-Verlag, Berlin, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30569-9_3","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-030-45237-7_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2020","unstructured":"Beyer, D.: Advances in automatic software verification: SV-COMP 2020. In: TACAS 2020. LNCS, vol. 12079, pp. 347\u2013367. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_21"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-030-72013-1_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2021","unstructured":"Beyer, D.: Software verification: 10th comparative evaluation (SV-COMP 2021). In: TACAS 2021. LNCS, vol. 12652, pp. 401\u2013422. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_24"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-030-99527-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2022","unstructured":"Beyer, D.: Progress on software verification: SV-COMP 2022. In: TACAS 2022. LNCS, vol. 13244, pp. 375\u2013402. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_20"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 300\u2013309. PLDI 2007, Association for Computing Machinery, New York, NY, USA (2007). https:\/\/doi.org\/10.1145\/1250734.1250769","DOI":"10.1145\/1250734.1250769"},{"key":"12_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., et al.: 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). https:\/\/doi.org\/10.1007\/3-540-36377-7_5"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-662-48288-9_9","volume-title":"Static Analysis","author":"M Brain","year":"2015","unstructured":"Brain, M., Joshi, S., Kroening, D., Schrammel, P.: Safety verification and refutation by $$k$$-invariants and $$k$$-induction. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 145\u2013161. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48288-9_9"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs by tiling. In: Proceedings of the 24th Static Analysis Symposium, pp. 428\u2013449 (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_21","DOI":"10.1007\/978-3-319-66706-5_21"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-030-45190-5_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Chakraborty","year":"2020","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs with full-program induction. In: TACAS 2020. LNCS, vol. 12078, pp. 22\u201339. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_2"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC\/Java2. In: Proceedings of the 4th International Conference on Formal Methods for Components and Objects, pp. 342\u2013363. FMCO 2005, Springer-Verlag, Berlin, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11804192_16","DOI":"10.1007\/11804192_16"},{"key":"12_CR13","first-page":"1","volume":"40","author":"HY Chen","year":"2017","unstructured":"Chen, H.Y., David, C., Kroening, D., Schrammel, P., Wachter, B.: Bit-precise procedure-modular termination proofs. ACM Trans. Prog. Lang. Syst. 40, 1\u201338 (2017)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"12_CR14","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). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation Functor for fully automatic and scalable array content analysis. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 105\u2013118. POPL 2011, Association for Computing Machinery, New York (2011). https:\/\/doi.org\/10.1145\/1926385.1926399","DOI":"10.1145\/1926385.1926399"},{"issue":"6","key":"12_CR16","doi-asserted-by":"publisher","first-page":"33:1","DOI":"10.1145\/1857914.1857917","volume":"57","author":"J Esparza","year":"2010","unstructured":"Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. J. ACM 57(6), 33:1-33:47 (2010). https:\/\/doi.org\/10.1145\/1857914.1857917","journal-title":"J. ACM"},{"issue":"7","key":"12_CR17","doi-asserted-by":"publisher","first-page":"805","DOI":"10.1142\/S0129054115400018","volume":"26","author":"J Esparza","year":"2015","unstructured":"Esparza, J., Luttenberger, M., Schlund, M.: FPSOLVE: a generic solver for fixpoint equations over semirings. Int. J. Found. Comput. Sci. 26(7), 805\u2013826 (2015). https:\/\/doi.org\/10.1142\/S0129054115400018","journal-title":"Int. J. Found. Comput. Sci."},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 191\u2013202. POPL 2002, Association for Computing Machinery, New York (2002). https:\/\/doi.org\/10.1145\/503272.503291","DOI":"10.1145\/503272.503291"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_38"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 338\u2013350. Association for Computing Machinery, New York (2005)","DOI":"10.1145\/1040305.1040333"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 235\u2013246. POPL 2008, Association for Computing Machinery, New York (2008). https:\/\/doi.org\/10.1145\/1328438.1328468","DOI":"10.1145\/1328438.1328468"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 339\u2013348. PLDI 2008, Association for Computing Machinery, New York (2008). https:\/\/doi.org\/10.1145\/1375581.1375623","DOI":"10.1145\/1375581.1375623"},{"key":"12_CR23","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: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193\u2013206. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_23"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Kroening, D., Mal\u00edk, V., Schrammel, P., Vojnar, T.: 2LS for Program Analysis. Tech. rep. (2023). https:\/\/doi.org\/10.48550\/arXiv.2302.02380","DOI":"10.48550\/arXiv.2302.02380"},{"key":"12_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-89960-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kumar","year":"2018","unstructured":"Kumar, S., Sanyal, A., Venkatesh, R., Shah, P.: Property checking array programs using loop shrinking. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 213\u2013231. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_12"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-540-27813-9_11","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2004","unstructured":"Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 135\u2013147. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_11"},{"key":"12_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-45069-6_15","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 141\u2013153. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_15"},{"key":"12_CR28","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). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_16"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"Mal\u00edk, V., Hru\u0161ka, M., Schrammel, P., Vojnar, T.: Template-based verification of heap-manipulating programs. In: Proceedings of the 2018 Formal Methods in Computer-Aided Design, pp. 103\u2013111 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603009","DOI":"10.23919\/FMCAD.2018.8603009"},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Mal\u00edk, V., Ne\u010das, F., Schrammel, P., Vojnar, T.: 2ls: Arrays and loop unwinding (competition contribution). In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023. Lecture Notes in Computer Science, vol. 13994, pp. 529\u2013534. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_31","DOI":"10.1007\/978-3-031-30820-8_31"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Schrammel, P., Kroening, D.: 2LS for program analysis - (competition contribution). In: Chechik, M., Raskin, JF. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2016. Lecture Notes in Computer Science, vol. 9636, pp. 905\u2013907. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_56","DOI":"10.1007\/978-3-662-49674-9_56"},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Shao, Z., Reppy, J.H., Appel, A.W.: Unrolling lists. In: Proceedings of the 1994 ACM Conference on LISP and Functional Programming, pp. 185\u2013195. Association for Computing Machinery, New York (1994). https:\/\/doi.org\/10.1145\/182409.182453","DOI":"10.1145\/182409.182453"}],"container-title":["Lecture Notes in Computer Science","Taming the Infinities of Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-56222-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,6]],"date-time":"2024-11-06T22:03:18Z","timestamp":1730930598000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-56222-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031562211","9783031562228"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-56222-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"20 March 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}