nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Loop Detection by Logically Constrained Term Rewriting

verfasst von : Naoki Nishida, Sarah Winkler

Erschienen in: Verified Software. Theories, Tools, and Experiments

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

Logically constrained rewrite systems constitute a very general rewriting formalism that can capture simplification processes in various domains as well as computation in imperative programs. In both of these contexts, nontermination is a critical source of errors. We present new criteria to find loops in logically constrained rewrite systems which are implemented in the tool Ctrl. We illustrate the usefulness of these criteria in three example applications: to find loops in LLVM peephole optimizations, to detect looping executions of C programs, and to establish nontermination of integer transition systems.

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 The Map Equality Domain

Nächstes Kapitel Store Buffer Reduction in the Presence of Mixed-Size Accesses and Misalignment

http://cl-informatik.uibk.ac.at/users/swinkler/lctrs_loops.

http://termination-portal.org/wiki/TPDB.

http://www.termination-portal.org/wiki/Termination_Competition_2017.

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRef

Borralleras, C., Brockschmidt, M., Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving termination through conditional termination. In: Legay, A., Margaria, T. (eds.) TACAS 2017. Heidelberg, vol. 10205, pp. 99–117. Springer, Cham (2017). https://doi.org/10.1007/978-3-662-54577-5_6CrossRef

Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: Temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387–393. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_22CrossRef

Falke, S., Kapur, D.: A term rewriting approach to the automated termination analysis of imperative programs. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 277–293. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_22CrossRefMATH

Falke, S., Kapur, D., Sinz, C.: Termination analysis of C programs using compiler intermediate languages. In: Proceedings of the 22nd RTA, Leibniz International Proceedings in Informatics, vol. 10, pp. 41–50 (2011). https://doi.org/10.4230/LIPIcs.RTA.2011.41

Fuhs, C., Giesl, J., Plücker, M., Schneider-Kamp, P., Falke, S.: Proving termination of integer term rewriting. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 32–47. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02348-4_3CrossRefMATH

Fuhs, C., Kop, C., Nishida, N.: Verifying procedural programs via constrained rewriting induction. ACM TOCL 18(2), 14:1–14:50 (2017). https://doi.org/10.1145/3060143MathSciNetCrossRefMATH

Ganesh, V., Berezin, S., Dill, D.: A decision procedure for fixed-width bit-vectors. Technical report, Stanford University (2005)

Giesl, J., et al.: Analyzing program termination and complexity automatically with AProVE. JAR 58(1), 3–31 (2017). https://doi.org/10.1007/s10817-016-9388-yMathSciNetCrossRefMATH

10.

Gupta, A., Henzinger, T., Majumdar, R., Rybalchenko, A., Xu, R.G.: Proving non-termination. SIGPLAN Not. 43(1), 147–158 (2008). https://doi.org/10.1145/1328897.1328459CrossRefMATH

11.

Hoder, K., Khasidashvili, Z., Korovin, K., Voronkov, A.: Preprocessing techniques for first-order clausification. In: Proceedings of the 12th FMCAD, pp. 44–51 (2012)

12.

Kop, C., Nishida, N.: Term rewriting with logical constraints. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 343–358. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40885-4_24CrossRef

13.

Kop, C., Nishida, N.: Constrained term rewriting tooL. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 549–557. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_38CrossRef

14.

Lopes, N., Menendez, D., Nagarakatte, S., Regehr, J.: Provably correct peephole optimizations with Alive. In: Proceedings of the 36th PLDI, pp. 22–32 (2015). https://doi.org/10.1145/2737924.2737965

15.

Lopes, N., Menendez, D., Nagarakatte, S., Regehr, J.: Practical verification of peephole optimizations with Alive. Commun. ACM 61(2), 84–91 (2018). https://doi.org/10.1145/3166064CrossRef

16.

Menendez, D., Nagarakatte, S.: Termination-checking for LLVM peephole optimizations. In: Proceedings of the 38th International Conference on Software Engineering, pp. 191–202 (2016). https://doi.org/10.1145/2884781.2884809

17.

Nadel, A.: Bit-vector rewriting with automatic rule generation. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 663–679. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_44CrossRef

18.

Nishida, N., Sakai, M., Hattori, T.: On disproving termination of constrained term rewriting systems. In: Proceedings of the 11th WST (2010)

19.

Payet, É.: Loop detection in term rewriting using the eliminating unfoldings. Theor. Comput. Sci. 403(2–3), 307–327 (2008). https://doi.org/10.1016/j.tcs.2008.05.013MathSciNetCrossRefMATH

Titel: Loop Detection by Logically Constrained Term Rewriting
verfasst von: Naoki Nishida
Sarah Winkler
Verlag: Springer International Publishing
Buch: Verified Software. Theories, Tools, and Experiments
Print ISBN: 978-3-030-03591-4

Electronic ISBN: 978-3-030-03592-1

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-030-03592-1_18

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"