Skip to main content
SpringerLink
Log in

Loop summarization using state and transition invariants

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

This paper presents algorithms for program abstraction based on the principle of loop summarization, which, unlike traditional program approximation approaches (e.g., abstract interpretation), does not employ iterative fixpoint computation, but instead computes symbolic abstract transformers with respect to a set of abstract domains. This allows for an effective exploitation of problem-specific abstract domains for summarization and, as a consequence, the precision of an abstract model may be tailored to specific verification needs. Furthermore, we extend the concept of loop summarization to incorporate relational abstract domains to enable the discovery of transition invariants, which are subsequently used to prove termination of programs. Well-foundedness of the discovered transition invariants is ensured either by a separate decision procedure call or by using abstract domains that are well-founded by construction.

We experimentally evaluate several abstract domains related to memory operations to detect buffer overflow problems. Also, our light-weight termination analysis is demonstrated to be effective on a wide range of benchmarks, including OS device drivers.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Algorithm 1
Algorithm 2
Algorithm 3
Fig. 2
Fig. 3

Similar content being viewed by others

Notes

  1. Here we only consider structured loops or loops for which the exit condition is evaluated before an iteration has changed the state of any variables.

  2. The Terminator algorithm is referred to as Binary Reachability Analysis (BRA), though BRA is only a particular technique to implement the algorithm (e.g., [21]).

  3. We discuss the relation of our method to size-change termination in Sect. 7.2.1.

  4. http://www.cprover.org/goto-cc/.

  5. http://www.cprover.org/loopfrog/.

  6. The data for all tools but Loopfrog, “=, ≠, ≤”, and the Interval Domain is from [61].

  7. We exclude those instances from our benchmarks.

  8. The corresponding bug reports may be obtained from http://cve.mitre.org/.

  9. However, the choice of transformer, i.e., “pre-condition” or “post-condition”, is irrelevant if only one step is performed.

  10. In this discussion we omit introducing the notation necessary for a formal description of SCT; see Lee et al. [36, 45] for more detail.

References

  1. Aiken A, Bugrara S, Dillig I, Dillig T, Hackett B, Hawkins P (2007) An overview of the Saturn project. In: Das M, Grossman D (eds) Workshop on program analysis for software tools and engineering. ACM, New York, pp 43–48

    Google Scholar 

  2. Ashcroft E, Manna Z (1979) The translation of ‘go to’ programs to ‘while’ programs. In: Classics in software engineering. Yourdon Press, Upper Saddle River, pp 49–61

    Google Scholar 

  3. Balaban I, Cohen A, Pnueli A (2006) Ranking abstraction of recursive programs. In: Emerson E, Namjoshi K (eds) Verification, model checking, and abstract interpretation (VMCAI). Lecture notes in computer science, vol 3855. Springer, Berlin, pp 267–281

    Chapter  Google Scholar 

  4. Ball T, Rajamani SK (2001) The SLAM toolkit. In: Computer aided verification (CAV). Lecture notes in computer science, vol 2102. Springer, Berlin, pp 260–264

    Chapter  Google Scholar 

  5. Ben-Amram AM, Lee CS (2009) Ranking functions for size-change termination II. In: Logical methods in computer science, vol 5. Chapter 8

    Google Scholar 

  6. Berdine J, Chawdhary A, Cook B, Distefano D, O’Hearn P (2007) Variance analyses from invariance analyses. In: Principles of programming languages (POPL). POPL’07. ACM, New York, pp 211–224. doi:10.1145/1190216.1190249

    Google Scholar 

  7. Beyer D, Henzinger TA, Théoduloz G (2006) Lazy shape analysis. In: Computer aided verification (CAV). Lecture notes in computer science, vol 4144. Springer, Berlin, pp 532–546

    Chapter  Google Scholar 

  8. Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:118–149

    Google Scholar 

  9. Cavada R, Cimatti A, Franzén A, Kalyanasundaram K, Roveri M, Shyamasundar RK (2007) Computing predicate abstractions by integrating BDDs and SMT solvers. In: Formal methods in computer-aided design (FMCAD). IEEE Computer Society, Los Alamitos, pp 69–76

    Google Scholar 

  10. Chaki S, Clarke EM, Groce A, Jha S, Veith H (2004) Modular verification of software components in C. IEEE Trans Softw Eng 30(6):388–402

    Article  Google Scholar 

  11. Chawdhary A, Cook B, Gulwani S, Sagiv M, Yang H (2008) Ranking abstractions. In: Drossopoulou S (ed) Programming languages and systems. Lecture notes in computer science, vol 4960. Springer, Berlin, pp 148–162

    Chapter  Google Scholar 

  12. Clarke E, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Emerson E, Sistla A (eds) Computer aided verification. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 154–169

    Chapter  Google Scholar 

  13. Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge

    Google Scholar 

  14. Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: Jensen K, Podelski A (eds) Tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol 2988. Springer, Berlin, pp 168–176

    Chapter  Google Scholar 

  15. Clarke EM, Kroening D, Sharygina N, Yorav K (2004) Predicate abstraction of ANSI-C programs using SAT. Form Methods Syst Des 25(2–3):105–127

    Article  MATH  Google Scholar 

  16. Clarke EM, Kroening D, Sharygina N, Yorav K (2005) SATABS: SAT-based predicate abstraction for ANSI-C. In: Tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science. Springer, Berlin, pp 570–574

    Chapter  Google Scholar 

  17. Cook B, Podelski A, Rybalchenko A (2005) Abstraction refinement for termination. In: International symposium on static analysis (SAS). Lecture notes in computer science, vol 3672. Springer, Berlin, pp 87–101

    Chapter  Google Scholar 

  18. Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: Programming language design and implementation (PLDI). ACM, New York, pp 415–426

    Google Scholar 

  19. Cook B, Gulwani S, Lev-Ami T, Rybalchenko A, Sagiv M (2008) Proving conditional termination. In: Computer aided verification (CAV). Lecture notes in computer science, vol 5123. Springer, Berlin, pp 328–340

    Chapter  Google Scholar 

  20. Cook B, Podelski A, Rybalchenko A (2009) Summarization for termination: no return! Form Methods Syst Des 35(3):369–387

    Article  MATH  Google Scholar 

  21. Cook B, Kroening D, Ruemmer P, Wintersteiger CM (2010) Ranking function synthesis for bit-vector relations. In: Tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol 6015. Springer, Berlin, pp 236–250

    Chapter  Google Scholar 

  22. Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of programming languages (POPL), pp 238–252

    Google Scholar 

  23. Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Principles of programming languages (POPL), pp 84–96

    Google Scholar 

  24. Dams D, Gerth R, Grumberg O (2000) A heuristic for the automatic generation of ranking functions. In: Proceedings of the workshop on advances in verification (WAVE), pp 1–8

    Google Scholar 

  25. Dor N, Rodeh M, Sagiv S (2003) CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In: Programming language design and implementation (PLDI), pp 155–167

    Google Scholar 

  26. D’Silva V, Haller L, Kroening D, Tautschnig M (2012) Numeric bounds analysis with conflict-driven learning. In: TACAS. Springer, Berlin, pp 48–63

    Google Scholar 

  27. Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for ESC/Java. In: Oliveira J, Zave P (eds) FME 2001: formal methods for increasing software productivity. Lecture notes in computer science. Springer, Berlin, pp 500–517

    Chapter  Google Scholar 

  28. Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R (2002) Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 conference on programming language design and implementation (PLDI’02). ACM, New York, pp 234–245. doi:10.1145/512529.512558

    Chapter  Google Scholar 

  29. Frama-C: http://frama-c.com/

  30. Gopan D, Reps TW (2007) Low-level library analysis and summarization. In: Computer aided verification (CAV). Lecture notes in computer science, vol 4590. Springer, Berlin, pp 68–81

    Chapter  Google Scholar 

  31. Graf S, Saidi H (1997) Construction of abstract state graphs with PVS. In: Computer aided verification (CAV). Lecture notes in computer science, vol 1254. Springer, Berlin, pp 72–83. doi:10.1007/3-540-63166-6_10

    Chapter  Google Scholar 

  32. Gulavani BS, Rajamani SK (2006) Counterexample driven refinement for abstract interpretation. In: Tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol 3920. Springer, Berlin, pp 474–488

    Chapter  Google Scholar 

  33. Gulavani BS, Chakraborty S, Nori AV, Rajamani SK (2010) Refining abstract interpretations. Inf Process Lett 110(16):666–671

    Article  MathSciNet  MATH  Google Scholar 

  34. Gulwani S, Lev-Ami T, Sagiv M (2009) A combination framework for tracking partition sizes. In: POPL’09: proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp 239–251. doi:10.1145/1480881.1480912

    Google Scholar 

  35. Gulwani S, Mehra KK, Chilimbi T (2009) Speed: precise and efficient static estimation of program computational complexity. In: POPL’09: proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp 127–139. doi:10.1145/1480881.1480898

    Google Scholar 

  36. Heizmann M, Jones N, Podelski A (2011) Size-change termination and transition invariants. In: Cousot R, Martel M (eds) Static analysis. Lecture notes in computer science, vol 6337. Springer, Berlin, pp 22–50

    Chapter  Google Scholar 

  37. Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Principles of programming languages (POPL). ACM, New York, pp 58–70

    Google Scholar 

  38. Hoare T (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580. doi:10.1145/363235.363259

    Article  MATH  Google Scholar 

  39. Jackson D, Vaziri M (2000) Finding bugs with a constraint solver. In: Proceedings of the international symposium on software testing and analysis (ISSTA), pp 14–25

    Chapter  Google Scholar 

  40. Kroening D, Sharygina N (2006) Approximating predicate images for bit-vector logic. In: Tools and algorithms for construction and analysis of systems (TACAS). Lecture notes in computer science, vol 3920. Springer, Berlin, pp 242–256

    Chapter  Google Scholar 

  41. Kroening D, Sharygina N, Tsitovich A, Wintersteiger CM (2010) Termination analysis with compositional transition invariants. In: International conference on computer-aided verification (CAV). Lecture notes in computer science, vol 6174. Springer, Edinburgh

    Google Scholar 

  42. Ku K, Hart TE, Chechik M, Lie D (2007) A buffer overflow benchmark for software model checkers. In: Automated software engineering (ASE). ACM, New York, pp 389–392

    Google Scholar 

  43. Lahiri SK, Ball T, Cook B (2005) Predicate abstraction via symbolic decision procedures. In: Computer aided verification (CAV). Lecture notes in computer science, vol 3576. Springer, Berlin, pp 24–38

    Chapter  Google Scholar 

  44. Lahiri SK, Nieuwenhuis R, Oliveras A (2006) SMT techniques for fast predicate abstraction. In: Computer aided verification (CAV). Lecture notes in computer science, vol 4144. Springer, Berlin, pp 424–437

    Chapter  Google Scholar 

  45. Lee CS, Jones ND, Ben-Amram AM (2001) The size-change principle for program termination. In: Principles of programming languages (POPL), vol 36. ACM, New York, pp 81–92. doi:10.1145/360204.360210

    Google Scholar 

  46. Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: Proceedings of the 16th international conference on logic for programming, artificial intelligence, and reasoning. Lecture notes in computer science, vol 6355. Springer, Berlin, pp 348–370. URL: http://dl.acm.org/citation.cfm?id=1939141.1939161

    Chapter  Google Scholar 

  47. Lev-Ami T, Sagiv S (2000) TVLA: a system for implementing static analyses. In: Static analysis (SAS). Lecture notes in computer science, vol 1824. Springer, Berlin, pp 280–301

    Chapter  Google Scholar 

  48. Manevich R, Field J, Henzinger TA, Ramalingam G, Sagiv M (2006) Abstract counterexample-based refinement for powerset domains. In: Program analysis and compilation (PAC). Lecture notes in computer science, vol 4444. Springer, Berlin, pp 273–292

    Chapter  Google Scholar 

  49. Moy Y (2009) Automatic modular static safety checking for C programs. PhD thesis, Université Paris-Sud. URL: http://www.lri.fr/~marche/moy09phd.pdf

  50. Podelski A, Rybalchenko A (2004) Transition invariants. In: IEEE symposium on logic in computer science (LICS). IEEE Computer Society, Los Alamitos, pp 32–41

    Google Scholar 

  51. Podelski A, Rybalchenko A (2007) ARMC: the logical choice for software model checking with abstraction refinement. In: Practical aspects of declarative languages (PADL). Springer, Berlin, pp 245–259

    Google Scholar 

  52. Reps T, Horwitz S, Sagiv M (1995) Precise interprocedural dataflow analysis via graph reachability. In: POPL’95: proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp 49–61. doi:10.1145/199448.199462

    Chapter  Google Scholar 

  53. Reps TW, Sagiv S, Yorsh G (2004) Symbolic implementation of the best transformer. In: Verification, model checking, and abstract interpretation (VMCAI). Lecture notes in computer science, vol 2937. Springer, Berlin, pp 252–266

    Chapter  Google Scholar 

  54. Scott J, Lee LH, Chin A, Arends J, Moyer B (1999) Designing the m⋅coretm m3 cpu architecture. In: International conference on computer design (ICCD), pp 94–101

    Google Scholar 

  55. Sharir M, Pnueli A (1981) Two approaches to interprocedural data flow analysis. In: Program flow analysis: theory and applications, Prentice-Hall, New York

    Google Scholar 

  56. SNU real-time benchmarks. http://archi.snu.ac.kr/realtime/benchmark/

  57. Suzuki N, Ishihata K (1977) Implementation of an array bound checker. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on principles of programming languages (POPL’77). ACM, New York, pp 132–143. doi:10.1145/512950.512963

    Google Scholar 

  58. Tarjan RE (1981) Fast algorithms for solving path problems. J ACM 28(3):594–614. http://doi.acm.org/10.1145/322261.322273

    Article  MathSciNet  MATH  Google Scholar 

  59. Turing AM (1936) On computable numbers, with an application to the entscheidungsproblem. Proc Lond Math Soc 2(42):230–265

    MathSciNet  Google Scholar 

  60. Turing AM (1949) Checking a large routine. In: Report of a conference on high speed automatic calculating machines. Cambridge, pp 67–69

    Google Scholar 

  61. Zitser M, Lippmann R, Leek T (2004) Testing static analysis tools using exploitable buffer overflows from open source code. In: International symposium on foundations of software engineering. ACM, New York, pp 97–106

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Oxford, Oxford, UK

    Daniel Kroening

  2. University of Lugano, Lugano, Switzerland

    Natasha Sharygina & Aliaksei Tsitovich

  3. Fondazione Bruno Kessler, Trento, Italy

    Stefano Tonetta

  4. Phonak AG, Stäfa, Switzerland

    Aliaksei Tsitovich

  5. Microsoft Research, Cambridge, UK

    Christoph M. Wintersteiger

Authors
  1. Daniel Kroening
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Natasha Sharygina
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Stefano Tonetta
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Aliaksei Tsitovich
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Christoph M. Wintersteiger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Aliaksei Tsitovich.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Kroening, D., Sharygina, N., Tonetta, S. et al. Loop summarization using state and transition invariants. Form Methods Syst Des 42, 221–261 (2013). https://doi.org/10.1007/s10703-012-0176-y

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-012-0176-y

Keywords

Search

Navigation