International School on Rewriting 2017
Advanced Track Course on
Proving Program Termination via Term Rewriting

Lecturer

Overview

Material

• The slides for the course (including exercises and their solutions in the appendix): Slides
• The Haskell source code for Exercises 1 and 2: Sources Exercise 1 and 2
• The termination proof found by AProVE for Exercise 1 is available here: Termination Proof Exercise 1
• The termination proof found by AProVE for Exercise 2 is available here: Termination Proof Exercise 2
• The Java source code for Exercise 4: Sources Exercise 4
• The Java source code for Exercise 5: Sources Exercise 5

Web Interface

Primary References

• 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
  Journal of Automated Reasoning, 58(1):3-31, 2017.
  The final publication is available at Springer via the DOI 10.1007/s10817-016-9388-y.
  Preliminary Version
• J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann
  Automated Termination Proofs for Haskell by Term Rewriting
  ACM Transactions on Programming Languages and Systems, 33(2), 2011.
  Preliminary Version
  
• C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl
  Automated Termination Analysis of Java Bytecode by Term Rewriting
  In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA '10), Edinburgh, UK, LIPIcs Leibniz International Proceedings in Informatics 6, pages 259-276, 2010. Dagstuhl Publishing