nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

13.11.2019 | General

On ranking functions for single-path linear-constraint loops

verfasst von: Yi Li, Wenyuan Wu, Yong Feng

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 6/2020

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Program termination is a fundamental research topic in program analysis. In this paper, we present a new complete polynomial-time method for the existence problem of linear ranking functions for single-path loops described by a conjunction of linear constraints, when variables range over the reals (or rationals). Unlike existing methods, our method does not depend on Farkas’ Lemma and provides us with counterexamples to existence of linear ranking functions, when no linear ranking function exists. In addition, we extend our results established over the rationals to the setting of the integers. This deduces an alternative approach to deciding whether or not a given SLC loop has a linear ranking function over the integers. Finally, we prove that the termination of bounded single-path linear-constraint loops is decidable over the reals (or rationals).

Nächster Artikel Enabling continuous integration in a formal methods setting

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

Alipranties, C., Border, K.: Infinite Dimensional Analysis: A Hitchhiker’s Guide. Springer, Berlin (2006)MATH

Bagnara, R., Mesnard, F.: Eventual linear ranking functions. In: PPDP’15, pp. 229–238. ACM, Madrid (2013)

Bagnara, R., Mesnard, F., Pescetti, A., Zaffanella, E.: A new look at the automatic synthesis of linear ranking functions. Inf. Comput. 215, 47–67 (2012)MathSciNetMATHCrossRef

Ben-Amram, A., Genaim, S.: On multiphase-linear ranking functions. In: Majumdar, R., Kunčak, V. (eds.) CAV’17, vol. 10427, pp. 601–620. Springer, Berlin (2017)

Ben-Amram, A., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4), 1–55 (2014)MathSciNetMATHCrossRef

Borwein, J., Moors, W.: Stability of closedness of convex cones under linear mappings. J. Conv. Anal. 16(2–4), 699–705 (2009)MathSciNetMATH

Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, New York (2004)MATHCrossRef

Bradley, A., Manna, Z., Sipma, H.: Linear ranking with reachability. In: Etessami, K., Rajamani, S. (eds.) CAV’05, vol. 3576, pp. 491–504. Springer, Berlin (2005)

Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R. (eds.) CAV’06, vol. 4144, pp. 372–385. Springer, Berlin (2006)

10.

Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering non-linear ranking functions by solving semi-algebraic systems. In: ICTAC’07, vol. 4711, pp. 34–49. Springer (2007)

11.

Colón, M., Sipma, H.: Synthesis of linear ranking functions. In: TACAS’01, vol. 2031, pp. 67–81. Springer (2001)

12.

Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS’13, vol. 7795, pp. 47–61. Springer (2013)

13.

Cousot, P.: Proving program invariance and termination by parametric abstraction, In: Lagrangian Relaxation and Semidefinite Programming. VMCAI’05, vol. 3385, pp. 1–24. Springer (2005)

14.

Duistermaat, J., Kolk, J.: Multidimensional Real Analysis. Cambridge University Press, Cambridge (2004)MATHCrossRef

15.

Feautrier, P.: Some efficient solutions to the affine scheduling problem. I. One-dimensional timed. Int. J. Paral. Prog. 21(5), 313–347 (1992)MathSciNetMATHCrossRef

16.

Floudas, C., Pardalos, P.: Encyclopedia of Optimization. Springer, Berlin (2009)MATHCrossRef

17.

Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: ATVA’13, vol. 8172, pp. 365–380. Springer (2013)

18.

Jing, R., Moreno Maza, M.: Computing the integer points of a polyhedron, I: algorithm. In: CASC2017, pp. 225–241. Springer (2017)

19.

Korte, B., Vygen, J.: Combinatorial Optimization: Theory and Algorithms, 5th edn. Springer, Berlin (2012)MATHCrossRef

20.

Leike, J., Heizmann, M.: Ranking templates for linear loops. Log. Methods Comput. Sci. 11(1), 1–27 (2015)MathSciNetMATHCrossRef

21.

Leike, J., Heizmann, M.: Geometric nontermination arguments. In: TACAS’18, vol. 10806, pp. 266–283. Springer (2018)

22.

Li, Y., Zhu, G., Feng, Y.: The L-depth eventual linear ranking functions for single-path linear constraints loops. In: TASE’16, pp. 30–37. IEEE (2016)

23.

Li, Y.: Witness to non-termination of linear programs. Theor. Comput. Sci. 681, 75–100 (2017)MathSciNetMATHCrossRef

24.

Liu, J., Xu, M., Zhan, N.J., Zhao, H.J.: Discovering non-terminating inputs for multi-path polynomial programs. J. Syst. Sci. Complex. 27, 1284–1304 (2014)MathSciNetMATH

25.

Ouaknine, J., Sousa Pinto, J., Worrell, J.: On termination of integer linear loops. In: SODA’15, pp. 957–69. SIAM (2015)

26.

Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: VMCAI’04, vol. 2937, pp. 239–251. Springer (2004)

27.

Rebiha,R., Matringe, N., Moura,A.: Generating asymptotically non-terminant initial variable values for linear diagonalizable programs. In: Symbolic Computation in Software Science, SCSS’13, pp. 81–92 (2013)

28.

Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)MATH

29.

Sohn, K., Gelder, A.: Termination detection in logic programs using argument sizes. In: Rosenkrantz, D.J. (ed.) Proceedings of the Symposium on Principles of Database Systems, pp. 216–226. ACM, New York (1991)

30.

Tiwari, A.: Termination of linear programs. In: CAV’04, pp. 70–82. Springer (2004)

Titel: On ranking functions for single-path linear-constraint loops
verfasst von: Yi Li
Wenyuan Wu
Yong Feng
Publikationsdatum: 13.11.2019
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 6/2020
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-019-00549-9

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 6/2020

An efficient statistical model checker for nondeterminism and rare events

Automating deductive verification for weak-memory programs (extended version)

AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic

Enabling continuous integration in a formal methods setting

Tools for the construction and analysis of systems

Efficient monitoring of hyperproperties using prefix trees