{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T09:50:33Z","timestamp":1774950633098,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642150241","type":"print"},{"value":"9783642150258","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-15025-8_15","type":"book-chapter","created":{"date-parts":[[2010,8,16]],"date-time":"2010-08-16T02:52:44Z","timestamp":1281927164000},"page":"277-300","source":"Crossref","is-referenced-by-count":32,"title":["Inferring Loop Invariants Using Postconditions"],"prefix":"10.1007","author":[{"given":"Carlo Alberto","family":"Furia","sequence":"first","affiliation":[]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","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.\u00a04349, pp. 378\u2013394. Springer, Heidelberg (2007)"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1145\/781131.781153","volume-title":"Proceedings of the 2003 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2003)","author":"B. 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 2003 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2003), pp. 196\u2013207. ACM, New York (2003)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-71067-7_15","volume-title":"Theorem Proving in Higher Order Logics","author":"S. B\u00f6hme","year":"2008","unstructured":"B\u00f6hme, S., Leino, K.R.M., Wolff, B.: HOL-Boogie \u2014 an interactive prover for the Boogie program-verifier. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 150\u2013166. Springer, Heidelberg (2008)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Moore, J.S.: MJRTY: A fast majority vote algorithm. In: Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 105\u2013118 (1991)","DOI":"10.1007\/978-94-011-3488-0_5"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/978-3-642-02658-4_15","volume-title":"CAV 2009","author":"M. Bozga","year":"2009","unstructured":"Bozga, M., Habermehl, P., Iosif, R., Kone\u010dn\u00fd, F., Vojnar, T.: Automatic verification of integer array programs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 157\u2013172. Springer, Heidelberg (2009)"},{"key":"15_CR6","volume-title":"The Calculus of Computation","author":"A.R. Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation. Springer, Heidelberg (2007)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"key":"15_CR8","unstructured":"de Caso, G., Garbervetsky, D., Gor\u00edn, D.: Reducing the number of annotations in a verification-oriented imperative language. In: Proceedings of Automatic Program Verification (2009)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-540-30579-8_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B.Y.E. Chang","year":"2005","unstructured":"Chang, B.Y.E., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 147\u2013163. Springer, Heidelberg (2005)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"15_CR11","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: Proceedings of the 4th Annual ACM Symposium on Principles of Programming Languages (POPL 1977), pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th Annual ACM Symposium on Principles of Programming Languages (POPL 1978), pp. 84\u201396 (1978)","DOI":"10.1145\/512760.512770"},{"key":"15_CR13","first-page":"281","volume-title":"Proceedings of the 30th International Conference on Software Engineering (ICSE 2008)","author":"C. Csallner","year":"2008","unstructured":"Csallner, C., Tillman, N., Smaragdakis, Y.: DySy: dynamic symbolic execution for invariant inference. In: Sch\u00e4fer, W., Dwyer, M.B., Gruhn, V. (eds.) Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), pp. 281\u2013290. ACM, New York (2008)"},{"key":"15_CR14","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"issue":"2","key":"15_CR15","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1109\/32.908957","volume":"27","author":"M.D. Ernst","year":"2001","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions of Software Engineering\u00a027(2), 99\u2013123 (2001)","journal-title":"IEEE Transactions of Software Engineering"},{"key":"15_CR16","unstructured":"Filli\u00e2tre, J.C.: The WHY verification tool (2009), version 2.18, \n                    \n                      http:\/\/proval.lri.fr"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 500\u2013517. Springer, Heidelberg (2001)"},{"key":"15_CR18","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201902). SIGPLAN Notices","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI\u201902). SIGPLAN Notices, vol.\u00a037(5), pp. 234\u2013245. ACM, New York (2002)"},{"key":"15_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The science of programming","author":"D. Gries","year":"1981","unstructured":"Gries, D.: The science of programming. Springer, Heidelberg (1981)"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-11319-2_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T.A. Henzinger","year":"2010","unstructured":"Henzinger, T.A., Hottelier, T., Kov\u00e1cs, L., Voronkov, A.: Invariant and type inference for matrices. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 163\u2013179. Springer, Heidelberg (2010)"},{"key":"15_CR21","unstructured":"Janota, M.: Assertion-based loop invariant generation. In: Proceedings of the 1st International Workshop on Invariant Generation, WING 2007 (2007)"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"C.M. Jean-Christophe Filli\u00e2tre","year":"2007","unstructured":"Jean-Christophe Filli\u00e2tre, C.M.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"15_CR23","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"key":"15_CR24","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.\u00a05503, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"15_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/978-3-642-02658-4_37","volume-title":"CAV 2009","author":"S.K. Lahiri","year":"2009","unstructured":"Lahiri, S.K., Qadeer, S., Galeotti, J.P., Voung, J.W., Wies, T.: Intra-module inference. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 493\u2013508. Springer, Heidelberg (2009)"},{"key":"15_CR26","unstructured":"Leino, K.R.M.: This is Boogie 2 (June 2008), (Manuscript KRML 178), \n                    \n                      http:\/\/research.microsoft.com\/en-us\/projects\/boogie\/"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: Shin, S.Y., Ossowski, S. (eds.) Proceedings of the 2009 ACM Symposium on Applied Computing (SAC 2009), pp. 615\u2013622. ACM Press, New York (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-24622-0_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F. Logozzo","year":"2004","unstructured":"Logozzo, F.: Automatic inference of class invariants. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 211\u2013222. Springer, Heidelberg (2004)"},{"key":"15_CR29","unstructured":"Meyer, B.: A basis for the constructive approach to programming. In: Lavington, S.H. (ed.) Proceedings of IFIP Congress 1980, pp. 293\u2013298 (1980)"},{"key":"15_CR30","volume-title":"Object-oriented software construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-oriented software construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"15_CR31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92145-5","volume-title":"Touch of Class: learning to program well with objects and contracts","author":"B. Meyer","year":"2009","unstructured":"Meyer, B.: Touch of Class: learning to program well with objects and contracts. Springer, Heidelberg (2009)"},{"key":"15_CR32","volume-title":"Programming from Specifications","author":"C. Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)","edition":"2"},{"key":"15_CR33","unstructured":"Parberry, I., Gasarch, W.: Problems on Algorithms (2002), \n                    \n                      http:\/\/www.eng.ent.edu\/ian\/books\/free\/"},{"key":"15_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-24732-6_13","volume-title":"Model Checking Software","author":"C.S. P\u0103s\u0103reanu","year":"2004","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 164\u2013181. Springer, Heidelberg (2004)"},{"key":"15_CR35","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/1029894.1029901","volume-title":"Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT 2004\/FSE-12)","author":"J.H. Perkings","year":"2004","unstructured":"Perkings, J.H., Ernst, M.D.: Efficient incremental algorithms for dynamic detection of likely invariants. In: Taylor, R.N., Dwyer, M.B. (eds.) Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT 2004\/FSE-12), pp. 23\u201332. ACM, New York (2004)"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Ciupa, I., Meyer, B.: A comparative study of programmer-written and automatically inferred contracts. In: Proceedings of the ACM\/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2009), pp. 93\u2013104 (2009)","DOI":"10.1145\/1572272.1572284"},{"issue":"4","key":"15_CR37","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","volume":"42","author":"E. Rodr\u00edguez-Carbonell","year":"2007","unstructured":"Rodr\u00edguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. Journal of Symbolic Computation\u00a042(4), 443\u2013476 (2007)","journal-title":"Journal of Symbolic Computation"},{"key":"15_CR38","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1145\/964001.964028","volume-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004)","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: Jones, N.D., Leroy, X. (eds.) Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), pp. 318\u2013329. ACM, New York (2004)"},{"key":"15_CR39","unstructured":"Schulte, W., Xia, S., Smans, J., Piessens, F.: A glimpse of a verifying C compiler (extended abstract). In: C\/C++ Verification Workshop (2007)"},{"key":"15_CR40","unstructured":"Tschannen, J.: Automatic verification of Eiffel programs. Master\u2019s thesis, Chair of Software Engineering, ETH Z\u00fcrich (2009)"}],"container-title":["Lecture Notes in Computer Science","Fields of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15025-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T17:16:33Z","timestamp":1558286193000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15025-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642150241","9783642150258"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15025-8_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}