{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:41:01Z","timestamp":1777347661924,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642005923","type":"print"},{"value":"9783642005930","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-00593-0_33","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T10:26:08Z","timestamp":1238149568000},"page":"470-485","source":"Crossref","is-referenced-by-count":88,"title":["Finding Loop Invariants for Programs over Arrays Using a Theorem Prover"],"prefix":"10.1007","author":[{"given":"Laura","family":"Kov\u00e1cs","sequence":"first","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"33_CR2","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., Majumdar, R., Rybalchenko, A.: Invariant Synthesis for Combined Theories. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 378\u2013394. Springer, Heidelberg (2007)"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"Beyer, D., Henzinger, T., Majumdar, R., Rybalchenko, A.: Path Invariants. In: Proc. of PLDI (2007)","DOI":"10.1145\/1250734.1250769"},{"key":"33_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-39910-0_11","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.\u00a02772, pp. 243\u2013268. Springer, Heidelberg (2004)"},{"key":"33_CR5","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: Proc. of POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program. In: Proc. of POPL, pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"issue":"8","key":"33_CR7","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Communications of the ACM\u00a018(8), 453\u2013457 (1975)","journal-title":"Communications of the ACM"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: Proc. of PLDI (2002)","DOI":"10.1145\/512529.512558"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: Predicate Abstraction for Software Verification. In: Proc. of POPL, pp. 191\u2013202 (2002)","DOI":"10.1145\/503272.503291"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T.W., Sagiv, M.: A Framework for Numeric Analysis of Array Operations. In: POPL, pp. 338\u2013350 (2005)","DOI":"10.1145\/1040305.1040333"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Gulwani, S., McCloskey, B., Tiwari, A.: Lifting Abstract Interpreters to Quantified Logical Domains. In: Proc. of POPL, pp. 235\u2013246 (2008)","DOI":"10.1145\/1328438.1328468"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-540-73368-3_42","volume-title":"Computer Aided Verification","author":"S. Gulwani","year":"2007","unstructured":"Gulwani, S., Tiwari, A.: An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 379\u2013392. Springer, Heidelberg (2007)"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., Peron, M.: Discovering Properties about Arrays in Simple Programs. In: Proc. of PLDI, pp. 339\u2013348 (2008)","DOI":"10.1145\/1375581.1375623"},{"key":"33_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/978-3-540-89439-1_24","volume-title":"LPAR","author":"T.A. Henzinger","year":"2008","unstructured":"Henzinger, T.A., Hottelier, T., Kovacs, L.: Valigator: A Verification Tool with Bound and Invariant Generation. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR. LNCS, vol.\u00a05330, pp. 333\u2013342. Springer, Heidelberg (2008)"},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"33_CR16","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.\u00a04590, pp. 193\u2013206. Springer, Heidelberg (2007)"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating Linear Arithmetic into Superposition Calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-78800-3_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Kovacs","year":"2008","unstructured":"Kovacs, L.: Reasoning Algebraically About P-Solvable Loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 249\u2013264. Springer, Heidelberg (2008)"},{"key":"33_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/11817963_16","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2006","unstructured":"Kroening, D., Weissenbacher, G.: Counterexamples with Loops for Predicate Abstraction. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 152\u2013165. Springer, Heidelberg (2006)"},{"key":"33_CR20","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":"S.K. 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.\u00a03114, pp. 135\u2013147. Springer, Heidelberg (2004)"},{"key":"33_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)"},{"key":"33_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-78800-3_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2008","unstructured":"McMillan, K.L.: Quantified Invariant Generation Using an Interpolating Saturation Prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 413\u2013427. Springer, Heidelberg (2008)"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Min\u00e9, A.: The Octagon Abstract Domain. In: Proc. of WCRE, pp. 310\u2013319 (2001)","DOI":"10.1109\/WCRE.2001.957836"},{"key":"33_CR24","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-Based Theorem Proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 7, vol.\u00a01, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"issue":"2-3","key":"33_CR25","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"33_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-25984-8_15","volume-title":"Automated Reasoning","author":"S. Schulz","year":"2004","unstructured":"Schulz, S.: System description: E\u00a00.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 223\u2013228. Springer, Heidelberg (2004)"},{"key":"33_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R.A., Hillenbrand, T., Rusev, R., Topic, D.: System description: spass version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00593-0_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T18:39:53Z","timestamp":1739039993000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00593-0_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005923","9783642005930"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00593-0_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}