Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 3/2013

01.06.2013

Loop summarization using state and transition invariants

verfasst von: Daniel Kroening, Natasha Sharygina, Stefano Tonetta, Aliaksei Tsitovich, Christoph M. Wintersteiger

Erschienen in: Formal Methods in System Design | Ausgabe 3/2013

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.
Nächster Artikel Event clock message passing automata: a logical characterization and an emptiness checking algorithm

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
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.
 
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.
 
Literatur
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 CrossRef
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 CrossRef
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. doi:10.​1145/​1190216.​1190249
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 CrossRef
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 CrossRef
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 CrossRef
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 CrossRef
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 CrossRef
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 MATHCrossRef
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 CrossRef
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 CrossRef
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 CrossRef
20.
Cook B, Podelski A, Rybalchenko A (2009) Summarization for termination: no return! Form Methods Syst Des 35(3):369–387 MATHCrossRef
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 CrossRef
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 CrossRef
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 CrossRef
29.
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 CrossRef
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 CrossRef
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 CrossRef
33.
Gulavani BS, Chakraborty S, Nori AV, Rajamani SK (2010) Refining abstract interpretations. Inf Process Lett 110(16):666–671 MathSciNetMATHCrossRef
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
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
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 CrossRef
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.
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 CrossRef
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 CrossRef
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 CrossRef
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 CrossRef
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
46.
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 CrossRef
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 CrossRef
49.
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. doi:10.​1145/​199448.​199462 CrossRef
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 CrossRef
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
55.
Sharir M, Pnueli A (1981) Two approaches to interprocedural data flow analysis. In: Program flow analysis: theory and applications, Prentice-Hall, New York
56.
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
58.
59.
Turing AM (1936) On computable numbers, with an application to the entscheidungsproblem. Proc Lond Math Soc 2(42):230–265 MathSciNet
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
Metadaten
Titel
Loop summarization using state and transition invariants
verfasst von
Daniel Kroening
Natasha Sharygina
Stefano Tonetta
Aliaksei Tsitovich
Christoph M. Wintersteiger
Publikationsdatum
01.06.2013
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 3/2013
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-012-0176-y

Premium Partner

    Bildnachweise