{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T07:49:16Z","timestamp":1771573756172,"version":"3.50.1"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"mail.ru group"},{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001711","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003475","name":"Hasler Stiftung","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003475","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2014,1]]},"abstract":"<jats:p>Software verification has emerged as a key concern for ensuring the continued progress of information technology. Full verification generally requires, as a crucial step, equipping each loop with a \u201cloop invariant.\u201d Beyond their role in verification, loop invariants help program understanding by providing fundamental insights into the nature of algorithms. In practice, finding sound and useful invariants remains a challenge. Fortunately, many invariants seem intuitively to exhibit a common flavor. Understanding these fundamental invariant patterns could therefore provide help for understanding and verifying a large variety of programs.<\/jats:p>\n          <jats:p>We performed a systematic identification, validation, and classification of loop invariants over a range of fundamental algorithms from diverse areas of computer science. This article analyzes the patterns, as uncovered in this study, governing how invariants are derived from postconditions; it proposes a taxonomy of invariants according to these patterns; and it presents its application to the algorithms reviewed. The discussion also shows the need for high-level specifications based on \u201cdomain theory.\u201d It describes how the invariants and the corresponding algorithms have been mechanically verified using an automated program prover; the proof source files are available. The contributions also include suggestions for invariant inference and for model-based specification.<\/jats:p>","DOI":"10.1145\/2506375","type":"journal-article","created":{"date-parts":[[2014,2,7]],"date-time":"2014-02-07T14:22:52Z","timestamp":1391782972000},"page":"1-51","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":50,"title":["Loop invariants"],"prefix":"10.1145","volume":"46","author":[{"given":"Carlo A.","family":"Furia","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[{"name":"ETH Zurich, ITMO St. Petersburg, and Eiffel Software, Zurich, Switzerland"}]},{"given":"Sergey","family":"Velder","sequence":"additional","affiliation":[{"name":"ITMO St. Petersburg, Saint Petersburg, Russia"}]}],"member":"320","published-online":{"date-parts":[[2014,1]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Handbook of Logic in Computer Science III","author":"Abramsky Samson","unstructured":"Samson Abramsky and Achim Jung . 1994. Domain theory . In Handbook of Logic in Computer Science III , S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (Eds.). Oxford University Press . Samson Abramsky and Achim Jung. 1994. Domain theory. In Handbook of Logic in Computer Science III, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (Eds.). Oxford University Press."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763048.1763087"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_2_1_4_1","unstructured":"Joshua Bloch. 2006. Extra Extra -- Read all about it: Nearly all binary searches and mergesorts are broken. http:\/\/googleresearch.blogspot.ch\/2006\/06\/extra-extra-read-all-about-it -nearly.html. (2006).  Joshua Bloch. 2006. Extra Extra -- Read all about it: Nearly all binary searches and mergesorts are broken. http:\/\/googleresearch.blogspot.ch\/2006\/06\/extra-extra-read-all-about-it -nearly.html. (2006)."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_15"},{"key":"e_1_2_1_6_1","volume-title":"Bradley and Zohar Manna","author":"Aaron","year":"2007","unstructured":"Aaron R. Bradley and Zohar Manna . 2007 . The Calculus of Computation. Springer . Aaron R. Bradley and Zohar Manna. 2007. The Calculus of Computation. Springer."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_11"},{"key":"e_1_2_1_10_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 1999 . Model Checking. MIT Press . Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_2_1_12_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","unstructured":"Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest , and Clifford Stein . 2009. Introduction to Algorithms ( 3 rd ed.). MIT Press . Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms (3rd ed.). MIT Press.","edition":"3"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368127"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of Automatic Program Verification.","author":"de Caso Guido","year":"2009","unstructured":"Guido de Caso , Diego Garbervetsky , and Daniel Gor\u00edn . 2009 . Reducing the number of annotations in a verification-oriented imperative language . In Proceedings of Automatic Program Verification. Guido de Caso, Diego Garbervetsky, and Daniel Gor\u00edn. 2009. Reducing the number of annotations in a verification-oriented imperative language. In Proceedings of Automatic Program Verification."},{"key":"e_1_2_1_17_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","unstructured":"Edsger W. Dijkstra . 1976. A Discipline of Programming . Prentice Hall . Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice Hall."},{"key":"e_1_2_1_18_1","unstructured":"Eiffel. 2006. Standard ECMA-367. Eiffel: Analysis design and programming language. (2006).  Eiffel. 2006. Standard ECMA-367. Eiffel: Analysis design and programming language. (2006)."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.908957"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of Symposia in Applied Mathematics Series","volume":"19","author":"Floyd Robert W.","year":"1967","unstructured":"Robert W. Floyd . 1967 . Assigning meanings to programs. In Mathematical Aspects of Computer Science J. T. Schwartz (Ed.) , Proceedings of Symposia in Applied Mathematics Series , vol. 19 . American Mathematical Society, 19--32. Robert W. Floyd. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science J. T. Schwartz (Ed.), Proceedings of Symposia in Applied Mathematics Series, vol. 19. American Mathematical Society, 19--32."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2011.53"},{"key":"e_1_2_1_22_1","series-title":"An CATCS Series","volume-title":"Modeling Time in Computing. Monographs in Theoretical Computer Science","author":"Furia Carlo A.","unstructured":"Carlo A. Furia , Dino Mandrioli , Angelo Morzenti , and Matteo Rossi . 2012. Modeling Time in Computing. Monographs in Theoretical Computer Science . An CATCS Series . Springer . Carlo A. Furia, Dino Mandrioli, Angelo Morzenti, and Matteo Rossi. 2012. Modeling Time in Computing. Monographs in Theoretical Computer Science. An CATCS Series. Springer."},{"key":"e_1_2_1_23_1","series-title":"Lecture Notes in Computer Science Series","volume-title":"Furia and Bertrand Meyer","author":"Carlo","year":"2010","unstructured":"Carlo A. Furia and Bertrand Meyer . 2010 . Inferring loop invariants using postconditions. In Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, Andreas Blass, Nachum Dershowitz, and Wolfgang Reisig (Eds.), Lecture Notes in Computer Science Series , vol. 6300 . Springer , 277--300. Carlo A. Furia and Bertrand Meyer. 2010. Inferring loop invariants using postconditions. In Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, Andreas Blass, Nachum Dershowitz, and Wolfgang Reisig (Eds.), Lecture Notes in Computer Science Series, vol. 6300. Springer, 277--300."},{"key":"e_1_2_1_24_1","volume-title":"Johnson","author":"Garey Michael R.","year":"1979","unstructured":"Michael R. Garey and David S . Johnson . 1979 . Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman . Michael R. Garey and David S. Johnson. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2009.5070542"},{"key":"e_1_2_1_26_1","volume-title":"The Science of Programming","author":"Gries David","unstructured":"David Gries . 1981. The Science of Programming . Springer-Verlag . David Gries. 1981. The Science of Programming. Springer-Verlag."},{"key":"e_1_2_1_27_1","volume-title":"18th IEEE International Conference on Automated Software Engineering (ASE\u201903)","author":"Gupta Neelam","unstructured":"Neelam Gupta and Zachary V. Heidepriem . 2003. A new structural coverage criterion for dynamic detection of program invariants . In 18th IEEE International Conference on Automated Software Engineering (ASE\u201903) . IEEE Computer Society, 49--59. Neelam Gupta and Zachary V. Heidepriem. 2003. A new structural coverage criterion for dynamic detection of program invariants. In 18th IEEE International Conference on Automated Software Engineering (ASE\u201903). IEEE Computer Society, 49--59."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187678"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_14"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/602382.602403"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 1st International Workshop on Invariant Generation (WING\u201907)","author":"Janota Mikol\u00e1\u0161","year":"2007","unstructured":"Mikol\u00e1\u0161 Janota . 2007 . Assertion-based loop invariant generation . In Proceedings of the 1st International Workshop on Invariant Generation (WING\u201907) . Mikol\u00e1\u0161 Janota. 2007. Assertion-based loop invariant generation. In Proceedings of the 1st International Workshop on Invariant Generation (WING\u201907)."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_2_1_36_1","volume-title":"Knapsack problems","author":"Kellerer Hans","unstructured":"Hans Kellerer , Ulrich Pferschy , and David Pisinger . 2004. Knapsack problems . Springer . Hans Kellerer, Ulrich Pferschy, and David Pisinger. 2004. Knapsack problems. Springer."},{"key":"e_1_2_1_37_1","volume-title":"The Art of Computer Programming","author":"Knuth Donald E.","year":"1968","unstructured":"Donald E. Knuth . 2011. The Art of Computer Programming ( 1 st ed., Volumes 1--4A). Addison-Wesley . 1968 --1973. Donald E. Knuth. 2011. The Art of Computer Programming (1st ed., Volumes 1--4A). Addison-Wesley. 1968--1973.","edition":"1"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00593-0_33"},{"key":"e_1_2_1_39_1","series-title":"An EATCS Series","volume-title":"Decision Procedures: An Algorithmic Point of View. Monographs in Theoretical Computer Sciences","author":"Kroening Daniel","year":"2008","unstructured":"Daniel Kroening and Ofer Strichman . 2008 . Decision Procedures: An Algorithmic Point of View. Monographs in Theoretical Computer Sciences . An EATCS Series . Springer . Daniel Kroening and Ofer Strichman. 2008. Decision Procedures: An Algorithmic Point of View. Monographs in Theoretical Computer Sciences. An EATCS Series. Springer."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_37"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1515698.1515713"},{"key":"e_1_2_1_43_1","volume-title":"This is Boogie 2. (June","author":"Leino K. Rustan M.","year":"2008","unstructured":"K. Rustan M. Leino . 2008. This is Boogie 2. (June 2008 ). ( Manuscript KRML 178) http:\/\/research.microsoft.com\/en-us\/projects\/boogie\/. K. Rustan M. Leino. 2008. This is Boogie 2. (June 2008). (Manuscript KRML 178) http:\/\/research.microsoft.com\/en-us\/projects\/boogie\/."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_18"},{"key":"e_1_2_1_45_1","volume-title":"Algorithms and Data Structures: The Basic Toolbox","author":"Mehlhorn Kurt","unstructured":"Kurt Mehlhorn and Peter Sanders . 2008. Algorithms and Data Structures: The Basic Toolbox . Springer . Kurt Mehlhorn and Peter Sanders. 2008. Algorithms and Data Structures: The Basic Toolbox. Springer."},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of IFIP Congress","author":"Meyer Bertrand","year":"1980","unstructured":"Bertrand Meyer . 1980 . A basis for the constructive approach to programming . In Proceedings of IFIP Congress 1980, Simon H. Lavington (Ed.). 293--298. Bertrand Meyer. 1980. A basis for the constructive approach to programming. In Proceedings of IFIP Congress 1980, Simon H. Lavington (Ed.). 293--298."},{"key":"e_1_2_1_47_1","volume-title":"Object-oriented software construction","author":"Meyer Bertrand","unstructured":"Bertrand Meyer . 1997. Object-oriented software construction ( 2 nd ed.). Prentice Hall . Bertrand Meyer. 1997. Object-oriented software construction (2nd ed.). Prentice Hall.","edition":"2"},{"key":"e_1_2_1_48_1","volume-title":"Programming from Specifications","author":"Morgan Carroll","unstructured":"Carroll Morgan . 1994. Programming from Specifications ( 2 nd ed.). Prentice Hall . Carroll Morgan. 1994. Programming from Specifications (2nd ed.). Prentice Hall.","edition":"2"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337304"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_1_51_1","volume-title":"Computational Complexity","author":"Papadimitriou Christos H.","unstructured":"Christos H. Papadimitriou . 1993. Computational Complexity . Addison-Wesley . Christos H. Papadimitriou. 1993. Computational Complexity. Addison-Wesley."},{"key":"e_1_2_1_52_1","volume-title":"P\u0103s\u0103reanu and Willem Visser","author":"Corina","year":"2004","unstructured":"Corina S. P\u0103s\u0103reanu and Willem Visser . 2004 . Verification of Java programs using symbolic execution and invariant generation. In Proceedings of the 11th International SPIN Workshop on Model Checking Software. Lecture Notes in Computer Science Series, vol. 2989 . Springer , 164--181. Corina S. P\u0103s\u0103reanu and Willem Visser. 2004. Verification of Java programs using symbolic execution and invariant generation. In Proceedings of the 11th International SPIN Workshop on Model Checking Software. Lecture Notes in Computer Science Series, vol. 2989. Springer, 164--181."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1029894.1029901"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn070"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572284"},{"key":"e_1_2_1_56_1","unstructured":"Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier.   Alan Robinson and Andrei Voronkov (Eds.). 2001. Handbook of Automated Reasoning. Elsevier."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2007.01.002"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964028"},{"key":"e_1_2_1_59_1","unstructured":"Michael I. Shamos. 1978. Computational geometry. Ph.D.thesis Yale University. http:\/\/goo.gl\/XiXNl.   Michael I. Shamos. 1978. Computational geometry. Ph.D.thesis Yale University. http:\/\/goo.gl\/XiXNl."},{"key":"e_1_2_1_60_1","volume-title":"Z Notation -- a reference manual","author":"Spivey J. Michael","unstructured":"J. Michael Spivey . 1992. Z Notation -- a reference manual ( 2 nd ed.). Prentice Hall International Series in Computer Science. Prentice Hall . J. Michael Spivey. 1992. Z Notation -- a reference manual (2nd ed.). Prentice Hall International Series in Computer Science. Prentice Hall.","edition":"2"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_39"},{"key":"e_1_2_1_62_1","volume-title":"Proceedings of IEEE MELECON.","author":"Toussaint Godfried T.","year":"1983","unstructured":"Godfried T. Toussaint . 1983 . Solving geometric problems with the rotating calipers . In Proceedings of IEEE MELECON. Godfried T. Toussaint. 1983. Solving geometric problems with the rotating calipers. In Proceedings of IEEE MELECON."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985820"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2011.6100094"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2506375","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2506375","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:44Z","timestamp":1750231724000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2506375"}},"subtitle":["Analysis, classification, and examples"],"short-title":[],"issued":{"date-parts":[[2014,1]]},"references-count":64,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,1]]}},"alternative-id":["10.1145\/2506375"],"URL":"https:\/\/doi.org\/10.1145\/2506375","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,1]]},"assertion":[{"value":"2012-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}