nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

20.04.2016 | TACAS 2013

Underapproximation of procedure summaries for integer programs

verfasst von: Pierre Ganty, Radu Iosif, Filip Konečný

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 5/2017

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We show how to underapproximate the procedure summaries of recursive programs over the integers using off-the-shelf analyzers for non-recursive programs. The novelty of our approach is that the non-recursive program we compute may capture unboundedly many behaviors of the original recursive program for which stack usage cannot be bounded. Moreover, we identify a class of recursive programs on which our method terminates and returns the precise summary relations without underapproximation. Doing so, we generalize a similar result for non-recursive programs to the recursive case. Finally, we present experimental results of an implementation of our method applied on a number of examples.

Vorheriger Artikel An integrated specification and verification technique for highly concurrent data structures

Nächster Artikel Efficient family-based model checking via variability abstractions

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

We adopt the convention that the empty sum evaluates to \({\mathbf {0}}\).

Observe that there are no global variables in the definition of integer program. Those can be encoded as input and output variables to each procedure.

Our simplified syntax does not seek to capture the generality of integer programs. Instead, our goal is to give a convenient notation for the programs given in this paper and only those.

assume \(\phi \) is executable if and only if the current values of the variables satisfy the Presburger formula \(\phi \).

havoc assigns non deterministically chosen integers to \(x_1,x_2,\ldots ,x_n\).

Recall that each \(w_i\) is a non-empty word.

Given two languages \(L_1 \subseteq \varSigma _1^*\) and \(L_2 \subseteq \varSigma _2^*\) their asynchronous product, denoted \(L_1 \parallel L_2\), is the language L over the alphabet \(\varSigma =\varSigma _1\cup \varSigma _2\) such that \(w\in L\) iff the projections of w to \(\varSigma _1\) and \(\varSigma _2\) belong to \(L_1\) and \(L_2\), respectively. Observe that the \(L_1\parallel L_2\) depends on \(L_1\), \(L_2\) and also their underlying alphabet \(\varSigma _1\) and \(\varSigma _2\).

https://github.com/filipkonecny/flata.

Lalire, G., Argoud, M., Jeannet, B.: Interproc. http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html

Atig, M.F., Ganty, P.: Approximating petri net reachability along context-free traces. In: FSTTCS’11, Volume 13 of LIPIcs, pp. 152–163. Schloss Dagstuhl, Wadern (2011)

Alur, R., Madhusudan, P.: Adding nesting structure to words. JACM 56(3), 16 (2009)MathSciNetCrossRefMATH

Hojjat, H., Konečný, F., Garnier, F., Iosif, R., Kuncak, V., Rümmer, P.: A verification toolkit for numerical transition systems—tool paper. In: FM 2012: Formal Methods, Volume 7436 of LNCS, pp. 247–251. Springer, Berlin, Heidelberg (2012)

Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, Chapter 7, pp. 189–233. Prentice-Hall, Inc., Upper Saddle River (1981)

Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. JACM 57(6), 33:1–33:47 (2010)MathSciNetCrossRefMATH

Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL’95, pp. 49–61. ACM, New York (1995)

Albarghouthi, A., Gurfinkel, A., Chechik, M.: Whale: an interpolation-based algorithm for inter-procedural verification. In: VMCAI’12, Volume 7148 of LNCS, pp. 39–55. Springer, Berlin (2012)

Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: POPL’10, pp. 43–56. ACM, New York (2010)

10.

Cook, A.P.B., Rybalchenko, A.: Summarization for termination: no return!. Formal Methods Syst. Design 35, 369–387 (2009)

11.

Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. In: CAV’13: Proc. 23rd Int. Conf. on Computer Aided Verification, LNCS, pp. 381–396. Springer, Berlin (2013)

12.

Latteux, M.: Mots infinis et langages commutatifs. Informatique Théorique et Appl. 12(3), 185–192 (1978)

13.

Luker, M.: Control sets on grammars using depth-first derivations. Math. Syst. Theory 13, 349–359 (1980)MathSciNetCrossRefMATH

14.

Ginsburg, S.: The Mathematical Theory of Context-Free Languages. McGraw-Hill Inc, New York (1966)MATH

15.

Bozga, M., Iosif, R., Konečný, F.: Fast acceleration of ultimately periodic relations. In: CAV’10, Volume 6174 of LNCS, pp. 227–242. Springer, Berlin (2010)

16.

Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, University of Liège (1998)

17.

Finkel, A., Leroux, J.: How to compose presburger-accelerations: applications to broadcast protocols. In: FSTTCS’02, Volume 2556 of LNCS, pp. 145–156. Springer, Berlin (2002)

18.

Luker, M.: A family of languages having only finite-index grammars. Inform. Control 39(1), 14–18 (1978)MathSciNetCrossRefMATH

19.

Godoy, G., Tiwari, A.: Invariant checking for programs with procedure calls. In: SAS’09, Volume 5673 of LNCS, pp. 326–342. Springer, Berlin (2009)

20.

Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: fast acceleration of symbolic transition systems. In: CAV’03, Volume 2725 of LNCS, pp. 118–121. Springer, Berlin (2003)

21.

Bozga, M., Iosif, R., Lakhnech, Y.: Flat parametric counter automata. Fundamenta Informaticae 91(2), 275–303 (2009)MathSciNetMATH

22.

Ganty, P., Majumdar, R., Monmege, B.: Bounded underapproximations. Formal Methods Syst. Design 40(2), 206–231 (2012)CrossRefMATH

23.

Termination Competition 2011. http://termcomp.uibk.ac.at/termcomp/home.seam

24.

Cowles, J.: Knuth’s generalization of mccarthy’s 91 function. In: Computer-Aided Reasoning: ACL2 Case Studies, pp. 283–299. Kluwer Academic Publishers, Berlin (2000)

Titel: Underapproximation of procedure summaries for integer programs
verfasst von: Pierre Ganty
Radu Iosif
Filip Konečný
Publikationsdatum: 20.04.2016
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 5/2017
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-016-0420-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"

Weitere Artikel der Ausgabe 5/2017

An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures

Advances in verification presented in TACAS’13

Synthesis of circular compositional program proofs via abduction

Flexible SAT-based framework for incremental bounded upgrade checking

Efficient family-based model checking via variability abstractions

metaSMT: focus on your application and not on solver integration