Document Open Access Logo

Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses (Invited Talk)

Author Georg Moser

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2017.2.pdf
  • Filesize: 0.52 MB
  • 10 pages

Document Identifiers

Subject Classification

Keywords
  • resource analysis
  • term rewriting
  • automation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

In this talk, I'll describe how rewriting techniques can be successfully employed to built state-of-the-art automated resource analysis tools which favourably compare to other approaches. Furthermore I'll sketch the genesis of a uniform framework for resource analysis, emphasising success stories, without hiding intricate weaknesses. The talk ends with the discussion of open problems.

Cite As Get BibTex

Georg Moser. Uniform Resource Analysis by Rewriting: Strenghts and Weaknesses (Invited Talk). In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.FSCD.2017.2

Author Details

Georg Moser

References

  1. E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost analysis of object-oriented bytecode programs. TCS, 413(1):142-159, 2012. Google Scholar
  2. E. Albert, S. Genaim, and A. N. Masud. On the inference of resource usage upper and lower bounds. TOCL, 14(3):22, 2013. Google Scholar
  3. R. Atkey. Amortised Resource Analysis with Separation Logic. LMCS, 7(2), 2011. Google Scholar
  4. M. Avanzini, U. Dal Lago, and G. Moser. Analysing the complexity of functional programs: Higher-order meets first-order. In Proc. 20th ICFP, pages 152-164. ACM, 2015. Google Scholar
  5. M. Avanzini and G. Moser. Tyrolean Complexity Tool: Features and Usage. In Proc. 24th RTA, volume 21 of LIPIcs, pages 71-80, 2013. Google Scholar
  6. M. Avanzini, G. Moser, and M. Schaper. TcT: Tyrolean Complexity Tool. In Proc. 22nd TACAS, LNCS, pages 407-423, 2016. Google Scholar
  7. M. Avanzini, C. Sternagel, and R. Thiemann. Certification of complexity proofs using ceta. In Proc. 26th RTA, volume 36 of LIPIcs, pages 23-39, 2015. Google Scholar
  8. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  9. A. Ben-Amram and S. Genaim. Ranking functions for linear-constraint loops. JACM, 61(4):26:1-26:55, 2014. URL: http://dx.doi.org/10.1145/2629488.
  10. R. Bird. Introduction to Functional Programming using Haskell, Second Edition. Prentice Hall, 1998. Google Scholar
  11. G. Bonfante, A. Cichon, J.-Y. Marion, and H. Touzet. Complexity classes and rewrite systems with polynomial interpretations. In Proc. 7th CSL, volume 1584 of LNCS, pages 372-384, 1998. Google Scholar
  12. G. Bonfante, A. Cichon, J.-Y. Marion, and H. Touzet. Algorithms with polynomial interpretation termination proof. JFP, 11(1):33-53, 2001. Google Scholar
  13. G. Bonfante, J.-Y. Marion, and J.-Y. Moyen. Quasi-interpretations a way to control resources. TCS, 412(25):2776-2796, 2011. Google Scholar
  14. M. Braverman. Termination of integer linear programs. In Proc. 18th CAV, volume 4144 of LNCS, pages 372-385, 2006. Google Scholar
  15. M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating runtime and size complexity analysis of integer programs. In Proc. 20th TACAS, volume 8413 of LNCS, pages 140-155, 2014. Google Scholar
  16. W. Buchholz. Proof-theoretical analysis of termination proofs. APAL, 75:57-65, 1995. Google Scholar
  17. E.-A. Cichon and P. Lescanne. Polynomial interpretations and the complexity of algorithms. In Proc. 11th CADE, volume 607 of LNCS, pages 139-147, 1992. Google Scholar
  18. E.-A. Cichon and A. Weiermann. Term rewriting theory for the primitive recursive functions. APAL, 83(3):199-223, 1997. Google Scholar
  19. U. Dal Lago. A short introduction to implicit computational complexity. In Lectures on Logic and Computation - ESSLLI 2010, volume 7388 of LNCS, pages 89-109, 2011. Google Scholar
  20. U. Dal Lago and M. Hofmann. Bounded linear logic, revisited. LMCS, 6(4), 2010. Google Scholar
  21. S. Falke and D. Kapur. A term rewriting approach to the automated termination analysis of imperative programs. In Proc. 22nd CADE, volume 5663 of LNCS, pages 277-293, 2009. Google Scholar
  22. A. Flores-Montoya. Upper and lower amortized cost bounds of programs expressed as cost relations. In Proc. 21st FM, volume 9995 of LNCS, 2016. URL: http://dx.doi.org/10.1007/978-3-319-48989-6_16.
  23. J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann. Analyzing program termination and complexity automatically with aprove. JAR, 58(1):3-31, 2017. URL: http://dx.doi.org/10.1007/s10817-016-9388-y.
  24. J.-Y. Girard, A. Scedrov, and P. Scott. Bounded linear logic: A modular approach to polynomial-time computability. TCS, 97(1):1-66, 1992. Google Scholar
  25. S. Gulwani and F. Zuleger. The reachability-bound problem. In Proc. PLDI'10, pages 292-304. ACM, 2010. Google Scholar
  26. V. Halava, T. Harju, M. Hirvensalo, and J. Karhumäki. Skolem’s Problem: On the Border Between Decidability and Undecidability. TUCS technical report. Turku Centre for Computer Science, 2005. Google Scholar
  27. D. Hofbauer. Termination proofs by multiset path orderings imply primitive recursive derivation lengths. TCS, 105:129-140, 1992. Google Scholar
  28. D. Hofbauer and C. Lautemann. Termination proofs and the length of derivations. In Proc. 3rd RTA, volume 355 of LNCS, pages 167-177, 1989. Google Scholar
  29. J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate amortized resource analysis. TOPLAS, 34(3):14, 2012. Google Scholar
  30. J. Hoffmann, A. Das, and S. Weng. Towards automatic resource bound analysis for OCaml. In Proc. 44th POPL, pages 359-373. ACM, 2017. Google Scholar
  31. J. Hoffmann and M. Hofmann. Amortized resource analysis with polynomial potential. In Proc. 19th ESOP, volume 6012 of LNCS, pages 287-306, 2010. Google Scholar
  32. M. Hofmann and G. Moser. Amortised resource analysis and typed polynomial interpretations. In Proc. of Joint 25th RTA and 12th TLCA, volume 8560 of LNCS, pages 272-286, 2014. Google Scholar
  33. M. Hofmann and G. Moser. Multivariate amortised resource analysis for term rewrite systems. In Proc. 13th TLCA, volume 38 of LIPIcs, pages 241-256, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.241.
  34. I. Lepper. Derivation lengths and order types of Knuth-Bendix orders. TCS, 269:433-450, 2001. Google Scholar
  35. A. Middeldorp, G. Moser, F. Neurauter, J. Waldmann, and H. Zankl. Joint spectral radius theory for automated complexity analysis of rewrite systems. In Proc. 4th CAI, volume 6742 of LNCS, pages 1-20, 2011. Google Scholar
  36. G. Moser. The Hydra battle and Cichon’s principle. AAECC, 20(2):133-158, 2009. URL: http://dx.doi.org/10.1007/s00200-009-0094-4.
  37. G. Moser. Proof theory at work: Complexity analysis of term rewrite systems. CoRR, abs/0907.5527, 2009. Habilitation Thesis. Google Scholar
  38. G. Moser and M. Schaper. A complexity preserving transformation from Jinja bytecode to rewrite systems. IC, 2017. To appear. Google Scholar
  39. G. Moser and A. Schnabl. The derivational complexity induced by the dependency pair method. LMCS, 7(3), 2011. Google Scholar
  40. G. Moser and A. Schnabl. Termination proofs in the dependency pair framework may induce multiple recursive derivational complexity. In Proc. 21st RTA, volume 10 of LIPIcs, pages 235-250, 2011. Google Scholar
  41. F. Nielson, H. R. Nielson, and C. Hankin. Principles of program analysis. Springer, 2005. Google Scholar
  42. T. Nipkow. Verified analysis of functional data structures. In 1st FSCD, pages 4:1-4:2, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSCD.2016.4.
  43. C. Okasaki. Purely functional data structures. Cambridge University Press, 1999. Google Scholar
  44. J. Ouaknine, J. S. Pinto, and J. Worrell. On termination of integer linear loops. In Proc. 26th SODA, pages 957-969. SIAM, 2015. Google Scholar
  45. A. Podelski and A. Rybalchenko. Transition predicate abstraction and fair termination. TOPLAS, 29(3), 2007. Google Scholar
  46. A. Podelski and Andrey Rybalchenko. A complete method for the synthesis of linear ranking functions. In Proc. 5th VMCAI, volume 2937 of LNCS, pages 239-251, 2004. Google Scholar
  47. M. Sinn, F. Zuleger, and H. Veith. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Proc. Software Engineering, volume 252 of LNI, pages 101-102, 2016. Google Scholar
  48. D. Sleator and R. Tarjan. Self-adjusting binary trees. In Proc. of the 15th STOC, pages 235-245. ACM, 1983. URL: http://dx.doi.org/10.1145/800061.808752.
  49. T. Tao. Structure and randomness: pages from year one of a mathematical blog. AMS, 2008. Google Scholar
  50. R. E. Tarjan. Amortized computational complexity. SIAM J. Alg. Disc. Meth, 6(2):306-318, 1985. Google Scholar
  51. TeReSe. Term Rewriting Systems, volume 55 of Cambridge Tracks in Theoretical Computer Science. Cambridge University Press, 2003. Google Scholar
  52. A. Tiwari. Termination of linear programs. In Proc. 16th CAV, volume 3114 of LNCS, pages 70-82, 2004. Google Scholar
  53. H. Touzet. Encoding the Hydra battle as a rewrite system. In Proc. 23rd MFCS, volume 1450 of LNCS, pages 267-276, 1998. Google Scholar
  54. A. Weiermann. Complexity bounds for some finite forms of Kruskal’s theorem. JSC, 18(5):463-488, November 1994. Google Scholar
  55. A. Weiermann. Termination proofs for term rewriting systems with lexicographic path ordering imply multiply recursive derivation lengths. TCS, 139:355-362, 1995. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact