nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

An Abstract Domain of Uninterpreted Functions

verfasst von : Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We revisit relational static analysis of numeric variables. Such analyses face two difficulties. First, even inexpensive relational domains scale too poorly to be practical for large code-bases. Second, to remain tractable they have extremely coarse handling of non-linear relations. In this paper, we introduce the subterm domain, a weakly relational abstract domain for inferring equivalences amongst sub-expressions, based on the theory of uninterpreted functions. This provides an extremely cheap approach for enriching non-relational domains with relational information, and enhances precision of both relational and non-relational domains in the presence of non-linear operations. We evaluate the idea in the context of the software verification tool SeaHorn.

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 Predicate Abstraction for Linked Data Structures

Nächstes Kapitel Property Directed Abstract Interpretation

We show transitive reductions and omit trivial bounds for variables. The result obtained by the subterm domain for C, includes, behind the scenes, a term equation \(t = u + s\) and a bound \(0 \le s \le 10\) on the freshly introduced variable s.

\(\sqsubseteq \) is extended to the term lattice by defining \(\bot \sqsubseteq t\) for all elements \(t \in \mathcal{T}_{/\equiv }\).

This behaviour is also a well recognized problem for finite domain constraint solvers (see e.g. [11]).

A program with its corresponding safety property also provided by the competition.

We used the command

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49122-5_4/395665_1_En_4_IEq362_HTML.gif

(i.e., large-block encoding [2] of the transition system modelling both pointer offsets and memory contents). For DD64 we add the option

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-49122-5_4/395665_1_En_4_IEq363_HTML.gif

We used an implementation of the classical DBM domain following [19] for the experiment in Table 2 but it took more than three hours to complete.

Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401–416. Springer, Heidelberg (2015)

Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Biere, A., Pixley, C., (eds.) Proceedings of the Ninth International Conference on Formal Methods in Computer-Aided Design, pp. 25–32. IEEE Computer Society (2009)

Bordeaux, L., Katsirelos, G., Narodytska, N., Vardi, M.Y.: The complexity of integer bound propagation. J. Artif. Intell. Res. (JAIR) 40, 657–676 (2011)MATHMathSciNet

Bouaziz, M.: TreeKs: a functor to make numerical abstract domains scalable. Electron. Notes Theor. Comput. Sci. 287, 41–52 (2012)CrossRef

Chang, B.-Y.E., M. Leino, K.R.: Abstract interpretation with alien expressions and heap structures. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 147–163. Springer, Heidelberg (2005) CrossRef

Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, pp. 106–130. Dunod (1976)

Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Logic Comput. 2(4), 511–547 (1992)MATHMathSciNetCrossRef

Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does Astrée scale up? Formal Meth. Syst. Des. 35(3), 229–264 (2009)MATHCrossRef

Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: Proceedings of the Fifth ACM Symposium on Principles of Programming Languages, pp. 84–97. ACM Press (1978)

10.

Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758–771 (1980)MATHMathSciNetCrossRef

11.

Feydy, T., Schutt, A., Stuckey, P.: Global difference constraint propagation for finite domain solvers. In: Antoy, S. (ed.) Proceedings of 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, pp. 226–235. ACM Press (2008)

12.

Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Abstract interpretation over non-lattice abstract domains. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 6–24. Springer, Heidelberg (2013) CrossRef

13.

Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Heidelberg (2015) CrossRef

14.

Howe, J.M., King, A.: Logahedra: a new weakly relational domain. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 306–320. Springer, Heidelberg (2009) CrossRef

15.

Huet, G.: Résolution d’Équations dans des Langages d’Ordre 1, 2, ..., \(\omega \). Thèse d’État. Université Paris VII (1976)

16.

Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846–862. Springer, Heidelberg (2013) CrossRef

17.

Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis and transformation. In: Proceedings of the International Symposium on Code Generation and Optimization, pp. 75–86. IEEE Computer Society (2004)

18.

Logozzo, F., Fähndrich, M.: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: Proceedings of the 2008 ACM Symposium on Applied Computing, pp. 184–188. ACM Press (2008)

19.

Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001) CrossRef

20.

Miné, A.: The octagon abstract domain. High. Ord. Symbolic Comput. 19(1), 31–100 (2006)MATHCrossRef

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 (2006) CrossRef

22.

Simon, A., King, A.: The two variable per inequality abstract domain. High. Ord. Symbolic Comput. 23(1), 87–143 (2010)MATHMathSciNetCrossRef

23.

Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 71–89. Springer, Heidelberg (2003) CrossRef

24.

Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, pp. 231–242. ACM Press (2004)

25.

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, Heidelberg (2012) CrossRef

Titel: An Abstract Domain of Uninterpreted Functions
verfasst von: Graeme Gange
Jorge A. Navas
Peter Schachte
Harald Søndergaard
Peter J. Stuckey
Verlag: Springer Berlin Heidelberg
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-662-49121-8

Electronic ISBN: 978-3-662-49122-5

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-662-49122-5_4

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"