Skip to main content
SpringerLink
Log in

Inferring Loop Invariants Using Postconditions

  • Chapter
Fields of Logic and Computation

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6300))

Abstract

One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop’s goal, also known as its contract); the present work takes advantage of this observation by using the postcondition as the basis for invariant inference, using various heuristics such as “uncoupling” which prove useful in many important algorithms. Thanks to these heuristics, the technique is able to infer invariants for a large variety of loop examples. We present the theory behind the technique, its implementation (freely available for download and currently relying on Microsoft Research’s Boogie tool), and the results obtained.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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–394. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  2. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, 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–207. ACM, New York (2003)

    Chapter  Google Scholar 

  3. Böhme, S., Leino, K.R.M., Wolff, B.: HOL-Boogie — an interactive prover for the Boogie program-verifier. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 150–166. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Boyer, R.S., Moore, J.S.: MJRTY: A fast majority vote algorithm. In: Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 105–118 (1991)

    Google Scholar 

  5. Bozga, M., Habermehl, P., Iosif, R., Konečný, F., Vojnar, T.: Automatic verification of integer array programs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 157–172. Springer, Heidelberg (2009)

    Google Scholar 

  6. Bradley, A.R., Manna, Z.: The Calculus of Computation. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  7. Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. de Caso, G., Garbervetsky, D., Gorín, D.: Reducing the number of annotations in a verification-oriented imperative language. In: Proceedings of Automatic Program Verification (2009)

    Google Scholar 

  9. Chang, B.Y.E., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 147–163. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Colón, 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. 2725, pp. 420–432. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  11. 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–252 (1977)

    Google Scholar 

  12. 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–96 (1978)

    Google Scholar 

  13. Csallner, C., Tillman, N., Smaragdakis, Y.: DySy: dynamic symbolic execution for invariant inference. In: Schäfer, W., Dwyer, M.B., Gruhn, V. (eds.) Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), pp. 281–290. ACM, New York (2008)

    Google Scholar 

  14. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  15. Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions of Software Engineering 27(2), 99–123 (2001)

    Article  Google Scholar 

  16. Filliâtre, J.C.: The WHY verification tool (2009), version 2.18, http://proval.lri.fr

  17. Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. 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’02). SIGPLAN Notices, vol. 37(5), pp. 234–245. ACM, New York (2002)

    Chapter  Google Scholar 

  19. Gries, D.: The science of programming. Springer, Heidelberg (1981)

    Book  MATH  Google Scholar 

  20. Henzinger, T.A., Hottelier, T., Kovács, L., Voronkov, A.: Invariant and type inference for matrices. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 163–179. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  21. Janota, M.: Assertion-based loop invariant generation. In: Proceedings of the 1st International Workshop on Invariant Generation, WING 2007 (2007)

    Google Scholar 

  22. Jean-Christophe Filliâtre, C.M.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  23. Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  24. Kovács, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470–485. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  25. 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. 5643, pp. 493–508. Springer, Heidelberg (2009)

    Google Scholar 

  26. Leino, K.R.M.: This is Boogie 2 (June 2008), (Manuscript KRML 178), http://research.microsoft.com/en-us/projects/boogie/

  27. 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–622. ACM Press, New York (2009)

    Google Scholar 

  28. Logozzo, F.: Automatic inference of class invariants. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 211–222. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  29. Meyer, B.: A basis for the constructive approach to programming. In: Lavington, S.H. (ed.) Proceedings of IFIP Congress 1980, pp. 293–298 (1980)

    Google Scholar 

  30. Meyer, B.: Object-oriented software construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)

    MATH  Google Scholar 

  31. Meyer, B.: Touch of Class: learning to program well with objects and contracts. Springer, Heidelberg (2009)

    Book  MATH  Google Scholar 

  32. Morgan, C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)

    MATH  Google Scholar 

  33. Parberry, I., Gasarch, W.: Problems on Algorithms (2002), http://www.eng.ent.edu/ian/books/free/

  34. Păsăreanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 164–181. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  35. 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–32. ACM, New York (2004)

    Chapter  Google Scholar 

  36. 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–104 (2009)

    Google Scholar 

  37. Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. Journal of Symbolic Computation 42(4), 443–476 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  38. Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gröbner 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–329. ACM, New York (2004)

    Chapter  Google Scholar 

  39. Schulte, W., Xia, S., Smans, J., Piessens, F.: A glimpse of a verifying C compiler (extended abstract). In: C/C++ Verification Workshop (2007)

    Google Scholar 

  40. Tschannen, J.: Automatic verification of Eiffel programs. Master’s thesis, Chair of Software Engineering, ETH Zürich (2009)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Chair of Software Engineering, ETH Zurich, Switzerland

    Carlo Alberto Furia & Bertrand Meyer

Authors
  1. Carlo Alberto Furia
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bertrand Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Mathematics Department, University of Michigan, 48109-1043, Ann Arbor, MI, USA

    Andreas Blass

  2. School of Computer Science, Tel Aviv University, Ramat Aviv, 69978, Tel Aviv, Israel

    Nachum Dershowitz

  3. Institut für Informatik, Humboldt-Universität zu Berlin, Unter den Linden 6, 10099, Berlin, Germany

    Wolfgang Reisig

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Furia, C.A., Meyer, B. (2010). Inferring Loop Invariants Using Postconditions. In: Blass, A., Dershowitz, N., Reisig, W. (eds) Fields of Logic and Computation. Lecture Notes in Computer Science, vol 6300. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15025-8_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15025-8_15

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15024-1

  • Online ISBN: 978-3-642-15025-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation