nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Structuring Abstract Interpreters Through State and Value Abstractions

verfasst von : Sandrine Blazy, David Bühler, Boris Yakobowski

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We present a new modular way to structure abstract interpreters. Modular means that new analysis domains may be plugged-in. These abstract domains can communicate through different means to achieve maximal precision. First, all abstractions work cooperatively to emit alarms that exclude the undesirable behaviors of the program. Second, the state abstract domains may exchange information through abstractions of the possible value for expressions. Those value abstractions are themselves extensible, should two domains require a novel form of cooperation. We used this approach to design \({\textsc {eva}}\), an abstract interpreter for C implemented within the \(\textsc {Frama}\text {-}\textsc {C}\) framework. We present the domains that are available so far within \({\textsc {eva}}\), and show that this communication mechanism is able to handle them seamlessly.

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 "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

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

Vorheriges Kapitel Reduction of Workflow Nets for Generalised Soundness Verification

Nächstes Kapitel Matching Multiplications in Bit-Vector Formulas

Directory src/plugins/value/ of the \(\textsc {Frama}\text {-}\textsc {C}\) source files, available at http://frama-c.com/download.html.

Bitfields, flexible array members and some GNU extensions are supported. Support for dynamic allocation is preliminary. Recursion, \(\texttt {{setjmp}/}{} \texttt {{longjmp}}\), \(\texttt {complex}\) types, \(\texttt {alloca}\) and variable-length arrays are not supported.

These are not undefined behaviors w.r.t. the ISO C99 or IEEE 754 specifications, but we choose to report them as undesirable errors.

Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221–239. Springer, Heidelberg (2006). doi:10.1007/11823230_15 CrossRef

Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: ASE, pp. 29–38 (2008)

Bonichon, R., Cuoq, P.: A mergeable interval map. Stud. Inform. Univ. 9(1), 5–37 (2011)

Boulanger, J.-L. (ed.): Static Analysis of Software: The Abstract Interpretation. Wiley-ISTE, New York (2011)

Brat, G., Navas, J.A., Shi, N., Venet, A.: IKOS: A framework for static analysis based on abstract interpretation. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 271–277. Springer, Cham (2014). doi:10.1007/978-3-319-10431-7_20

Cortesi, A., Le Charlier, B., Van Hentenryck, P.: Combinations of abstract domains for logic programming: open product and generic pattern construction. Sci. Comput. Program. 38(1–3), 27–71 (2000)MathSciNetCrossRefMATH

Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. In: Essays Dedicated to D. Schmidt on the Occasion of his 60th Birthday, pp. 325–336 (2013)

Cousot, P.: The calculational design of a generic abstract interpreter. In: Calculational System Design. NATO ASI Series F. IOS Press (1999)

Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, pp. 238–252 (1977)

10.

Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Principles of Programming Languages, pp. 269–282 (1979)

11.

Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Combination of abstractions in the ASTRÉE static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2007). doi:10.1007/978-3-540-77505-8_23 CrossRef

12.

Cuoq, P., Hilsenkopf, P., Kirchner, F., Labbé, S., Thuy, N., Yakobowski, B.: Formal verification of software important to safety using the Frama-C tool suite. In: NPIC & HMIT (2012)

13.

Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Berlin (2011). doi:10.1007/978-3-642-18070-5_2 CrossRef

14.

International Organization for Standardization (ISO). International Standard ISO/IEC 9899: 1999 - Programming languages - C. Technical Corrigendum 3 (2007)

15.

Jeannet, B., Miné, A.: Apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Berlin (2009). doi:10.1007/978-3-642-02658-4_52 CrossRef

16.

Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Principles of Programming Language, pp. 247–259 (2015)

17.

Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A software analysis perspective. Formal Asp. Comput. 27(3), 573–609 (2015)MathSciNetCrossRef

18.

Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Berlin (2005). doi:10.1007/978-3-540-31987-0_2 CrossRef

19.

Miné, A.: The octagon abstract domain. In: Burd, E., Aiken, P., Koschke, R. (eds.) Proceedings of the Eighth Working Conference on Reverse Engineering, WCRE 2001, Stuttgart, Germany, 2–5 October 2001, p. 310. IEEE Computer Society (2001)

20.

Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: LCTES, pp. 54–63. ACM (2006)

21.

Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2005). doi:10.1007/11609773_23 CrossRef

22.

Venet, A.J.: The gauge domain: scalable analysis of linear inequality invariants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 139–154. Springer, Berlin (2012). doi:10.1007/978-3-642-31424-7_15 CrossRef

23.

Yakobowski, B.: Fast whole-program verification using on-the-fly summarization. In: Workshop on Tools for Automatic Program Analysis (2015)

Titel: Structuring Abstract Interpreters Through State and Value Abstractions
verfasst von: Sandrine Blazy
David Bühler
Boris Yakobowski
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-319-52233-3

Electronic ISBN: 978-3-319-52234-0

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-52234-0_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"