[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Finding and Certifying Loops

  • Conference paper
SOFSEM 2010: Theory and Practice of Computer Science (SOFSEM 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5901))

Abstract

The first part of this paper presents a new approach for automatically proving nontermination of string rewrite systems. We encode rewrite sequences as propositional formulas such that a loop can be extracted from a satisfying assignment. Alternatively, loops can be found by enumerating forward closures. In the second part we give a formalization of loops in the theorem prover Isabelle/HOL. Afterwards, we use Isabelle’s code-generation facilities to certify loops. The integration of our approach in CeTA (a program for automatic certification of termination proofs) makes it the first tool capable of certifying nontermination.

This research is supported by FWF (Austrian Science Fund) project P18763.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 71.50
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 89.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Arts, T., Giesl, J.: Termination of Term Rewriting Using Dependency Pairs. TCS 236(1-2), 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  3. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development; Coq’Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science. An EATCS Series (2004)

    Google Scholar 

  4. Blanqui, F., Delobel, W., Coupet-Grimal, S., Hinderer, S., Koprowski, A.: COLOR, a COQ Library on Rewriting and Termination. In: WST, pp. 69–73 (2006)

    Google Scholar 

  5. Clarke, A., Biere, A., Raimi, R., Zhu, Y.: Bounded Model Checking Using Satisfiability Solving. FMSD 19(1), 7–34 (2001)

    MATH  Google Scholar 

  6. Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Certification of Automated Termination Proofs. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 148–162. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Cook, S.: The Complexity of Theorem-Proving Procedures. In: STOC, pp. 151–158 (1971)

    Google Scholar 

  8. Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  9. Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Google Scholar 

  10. Endrullis, J., Waldmann, J., Zantema, H.: Matrix Interpretations for Proving Termination of Term Rewriting. JAR 40(2-3), 195–220 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  11. Geser, A., Hofbauer, D., Waldmann, J.: Termination Proofs for String Rewriting Systems via Inverse Match-Bounds. JAR 34(4), 365–385 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  12. Geser, A., Zantema, H.: Non-Looping String Rewriting. TIA 33(3), 279–302 (1999)

    MATH  MathSciNet  Google Scholar 

  13. Giesl, J., Thiemann, R., Schneider-Kamp, P.: The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 301–331. Springer, Heidelberg (2005)

    Google Scholar 

  14. Giesl, J., Thiemann, R., Schneider-Kamp, P.: Proving and Disproving Termination of Higher-Order Functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 216–231. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  15. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and Improving Dependency Pairs. JAR 37(3), 155–203 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  16. Haftmann, F.: Code Generation from Specifications in Higher Order Logic. PhD Thesis, Technische Universität München (2009)

    Google Scholar 

  17. Hirokawa, N., Middeldorp, A.: Automating the Dependency Pair Method. I&C 199(1-2), 172–199 (2005)

    MATH  MathSciNet  Google Scholar 

  18. Korp, M., Middeldorp, A.: Match-Bounds Revisited. I&C (2009), doi:10.1016/j.ic.2009.02.010

    Google Scholar 

  19. Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean Termination Tool 2. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 295–304. Springer, Heidelberg (2009)

    Google Scholar 

  20. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  21. Oppelt, M.: Automatische Erkennung von Ableitungsmustern in nichtterminierenden Wortersetzungssystemen. Master’s Thesis, HTWK Leipzig, FH (2008)

    Google Scholar 

  22. Payet, É.: Loop Detection in Term Rewriting Using the Eliminating Unfoldings. TCS 403(2-3), 307–327 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  23. Plaisted, D., Greenbaum, S.: A Structure-Preserving Clause Form Translation. JSC 2(3), 293–304 (1986)

    MATH  MathSciNet  Google Scholar 

  24. Thiemann, R., Sternagel, C.: Certification of Termination Proofs Using CeTA. In: Berghofer, S., et al. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452–468. Springer, Heidelberg (2009)

    Google Scholar 

  25. Waldmann, J.: Matchbox: A Tool for Match-Bounded String Rewriting. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 85–94. Springer, Heidelberg (2004)

    Google Scholar 

  26. Waldmann, J.: Compressed Loops, Draft (2007), http://dfa.imn.htwk-leipzig.de/matchbox/methods/loop.pdf

  27. Zankl, H.: Lazy Termination Analysis. PhD Thesis, University of Innsbruck (2009)

    Google Scholar 

  28. Zantema, H.: Termination of String Rewriting Proved Automatically. JAR 34(2), 105–139 (2005)

    Google Scholar 

  29. Zantema, H.: Termination. In: TeReSe (ed.) Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55, pp. 181–259. Cambridge University Press, Cambridge (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zankl, H., Sternagel, C., Hofbauer, D., Middeldorp, A. (2010). Finding and Certifying Loops. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds) SOFSEM 2010: Theory and Practice of Computer Science. SOFSEM 2010. Lecture Notes in Computer Science, vol 5901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11266-9_63

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11266-9_63

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11265-2

  • Online ISBN: 978-3-642-11266-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics