Formal Methods in System Design

, Volume 42, Issue 3, pp 221–261 | Cite as

Loop summarization using state and transition invariants

  • Daniel Kroening
  • Natasha Sharygina
  • Stefano Tonetta
  • Aliaksei Tsitovich
  • Christoph M. Wintersteiger
Article

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.

Keywords

Program abstraction Loop summarization Loop invariants Transition invariants Termination 

References

  1. 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. 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. 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 CrossRefGoogle Scholar
  4. 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 CrossRefGoogle Scholar
  5. 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. 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. 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 CrossRefGoogle Scholar
  8. 8.
    Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:118–149 Google Scholar
  9. 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. 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 CrossRefGoogle Scholar
  11. 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 CrossRefGoogle Scholar
  12. 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 CrossRefGoogle Scholar
  13. 13.
    Clarke EM, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge Google Scholar
  14. 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 CrossRefGoogle Scholar
  15. 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 MATHCrossRefGoogle Scholar
  16. 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 CrossRefGoogle Scholar
  17. 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 CrossRefGoogle Scholar
  18. 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. 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 CrossRefGoogle Scholar
  20. 20.
    Cook B, Podelski A, Rybalchenko A (2009) Summarization for termination: no return! Form Methods Syst Des 35(3):369–387 MATHCrossRefGoogle Scholar
  21. 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 CrossRefGoogle Scholar
  22. 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. 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. 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. 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. 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. 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 CrossRefGoogle Scholar
  28. 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 CrossRefGoogle Scholar
  29. 29.
  30. 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 CrossRefGoogle Scholar
  31. 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 CrossRefGoogle Scholar
  32. 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 CrossRefGoogle Scholar
  33. 33.
    Gulavani BS, Chakraborty S, Nori AV, Rajamani SK (2010) Refining abstract interpretations. Inf Process Lett 110(16):666–671 MathSciNetMATHCrossRefGoogle Scholar
  34. 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. 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. 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 CrossRefGoogle Scholar
  37. 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. 38.
    Hoare T (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580. doi:10.1145/363235.363259 MATHCrossRefGoogle Scholar
  39. 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 CrossRefGoogle Scholar
  40. 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 CrossRefGoogle Scholar
  41. 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. 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. 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 CrossRefGoogle Scholar
  44. 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 CrossRefGoogle Scholar
  45. 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. 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 CrossRefGoogle Scholar
  47. 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 CrossRefGoogle Scholar
  48. 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 CrossRefGoogle Scholar
  49. 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. 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. 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. 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 CrossRefGoogle Scholar
  53. 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 CrossRefGoogle Scholar
  54. 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. 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. 56.
    SNU real-time benchmarks. http://archi.snu.ac.kr/realtime/benchmark/
  57. 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. 58.
    Tarjan RE (1981) Fast algorithms for solving path problems. J ACM 28(3):594–614. http://doi.acm.org/10.1145/322261.322273 MathSciNetMATHCrossRefGoogle Scholar
  59. 59.
    Turing AM (1936) On computable numbers, with an application to the entscheidungsproblem. Proc Lond Math Soc 2(42):230–265 MathSciNetGoogle Scholar
  60. 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. 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

Copyright information

© Springer Science+Business Media New York 2012

Authors and Affiliations

  • Daniel Kroening
    • 1
  • Natasha Sharygina
    • 2
  • Stefano Tonetta
    • 3
  • Aliaksei Tsitovich
    • 2
    • 4
  • Christoph M. Wintersteiger
    • 5
  1. 1.University of OxfordOxfordUK
  2. 2.University of LuganoLuganoSwitzerland
  3. 3.Fondazione Bruno KesslerTrentoItaly
  4. 4.Phonak AGStäfaSwitzerland
  5. 5.Microsoft ResearchCambridgeUK

Personalised recommendations