article

Loop summarization using state and transition invariants

Authors:

Daniel Kroening,

Natasha Sharygina,

Stefano Tonetta,

Aliaksei Tsitovich,

Christoph M. WintersteigerAuthors Info & Claims

Formal Methods in System Design, Volume 42, Issue 3

Pages 221 - 261

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

Published: 01 June 2013 Publication History

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.

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.

[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.

[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.

[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.

[5]

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

[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.

[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.

[8]

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

[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.

[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.

Digital Library

[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.

[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.

[13]

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

[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.

[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.

Digital Library

[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.

[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.

[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.

[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.

[20]

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

[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.

[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.

[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.

[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.

[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.

[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.

[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.

[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.

[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.

[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.

[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.

[33]

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

Digital Library

[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.

[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 SIGPLANSIGACT symposium on principles of programming languages. ACM, New York, pp 127-139.

[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.

[37]

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

[38]

Hoare T (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576-580.

Digital Library

[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.

[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.

[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.

[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.

[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.

[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.

[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. 360210.

[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.

[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.

[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.

[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.

[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.

[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.

[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.

[54]

Scott J, Lee LH, Chin A, Arends J, Moyer B (1999) Designing the m¿core^tm m3 cpu architecture. In: International conference on computer design (ICCD), pp 94-101.

[55]

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

Digital Library

[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.

[58]

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

Digital Library

[59]

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

[60]

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

[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.

Cited By

Heim PDimitrova R(2024)Solving Infinite-State Games via AccelerationProceedings of the ACM on Programming Languages10.1145/36328998:POPL(1696-1726)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632899
Schmuck AHeim PDimitrova RNayak S(2024)Localized Attractor Computations for Infinite-State GamesComputer Aided Verification10.1007/978-3-031-65633-0_7(135-158)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_7
Shi QXu XZhang XCalandrino JTroncoso C(2023)Extracting protocol format as state machine via controlled static loop analysisProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620630(7019-7036)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620630
Show More Cited By

Loop summarization using state and transition invariants

Recommendations

S-looper: automatic summarization for multipath string loops
ISSTA 2015: Proceedings of the 2015 International Symposium on Software Testing and Analysis

Loops are important yet most challenging program constructs to analyze for various program analysis tasks. Existing loop analysis techniques mainly handle well loops that contain only integer variables with a single path in the loop body. The key ...
Static loop analysis and its applications
FSE 2016: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering

Loops are challenging structures in program analysis, and an effective loop analysis is crucial in the applications, such as symbolic execution and program verification. In the research, we will first perform a deep analysis and propose a ...
Algebraic Tools for Computing Polynomial Loop Invariants
ISSAC '24: Proceedings of the 2024 International Symposium on Symbolic and Algebraic Computation

Loop invariants are properties of a program loop that hold before and after each iteration of the loop. They are often employed to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Methods in System Design

Formal Methods in System Design Volume 42, Issue 3

June 2013

107 pages

ISSN:0925-9856

Issue’s Table of Contents

Copyright © Copyright © 2013 Springer Science+Business Media New York.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 June 2013

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Heim PDimitrova R(2024)Solving Infinite-State Games via AccelerationProceedings of the ACM on Programming Languages10.1145/36328998:POPL(1696-1726)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632899
Schmuck AHeim PDimitrova RNayak S(2024)Localized Attractor Computations for Infinite-State GamesComputer Aided Verification10.1007/978-3-031-65633-0_7(135-158)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_7
Shi QXu XZhang XCalandrino JTroncoso C(2023)Extracting protocol format as state machine via controlled static loop analysisProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620630(7019-7036)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620630
Blicha MKofroň JTatarko WHong JBures MPark JCerny T(2022)Summarization of branching loopsProceedings of the 37th ACM/SIGAPP Symposium on Applied Computing10.1145/3477314.3507042(1808-1816)Online publication date: 25-Apr-2022
https://dl.acm.org/doi/10.1145/3477314.3507042
Kleine Büning MSinz CFaragó D(2020)QPR Verify: A Static Analysis Tool for Embedded Software Based on Bounded Model CheckingSoftware Verification10.1007/978-3-030-63618-0_2(21-32)Online publication date: 19-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-63618-0_2
Awadhutkar PSanthanam GHolland BKothari SDumas MPfahl DApel SRusso A(2019)DISCOVER: detecting algorithmic complexity vulnerabilitiesProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3338906.3341177(1129-1133)Online publication date: 12-Aug-2019
https://dl.acm.org/doi/10.1145/3338906.3341177
Alatawi ESøndergaard HMiller TRosu GDi Penta MNguyen T(2017)Leveraging abstract interpretation for efficient dynamic symbolic executionProceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering10.5555/3155562.3155639(619-624)Online publication date: 30-Oct-2017
https://dl.acm.org/doi/10.5555/3155562.3155639
Fedyukovich GSery OSharygina N(2017)Flexible SAT-based framework for incremental bounded upgrade checkingInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-015-0405-y19:5(517-534)Online publication date: 1-Oct-2017
https://dl.acm.org/doi/10.1007/s10009-015-0405-y
Xiaofei XZimmermann TCleland-Huang JSu Z(2016)Static loop analysis and its applicationsProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2950290.2983972(1130-1132)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2950290.2983972
Xie XChen BLiu YLe WLi XZimmermann TCleland-Huang JSu Z(2016)Proteus: computing disjunctive loop summary via path dependency analysisProceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering10.1145/2950290.2950340(61-72)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1145/2950290.2950340

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents