References

  1. Beatriz Alarcón, Fabian Emmes, Carsten Fuhs, Jürgen Giesl, Raúl Gutiérrez, Salvador Lucas, Peter Schneider-Kamp & René Thiemann (2008): Improving Context-Sensitive Dependency Pairs. In: Iliano Cervesato, Helmut Veith & Andrei Voronkov: Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science 5330. Springer, pp. 636–651, doi:10.1007/978-3-540-89439-1_44.
  2. Thomas Arts & Jürgen Giesl (2000): Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1-2), pp. 133–178, doi:10.1016/S0304-3975(99)00207-8.
  3. Franz Baader & Tobias Nipkow (1998): Term Rewriting and All That. Cambridge University Press, doi:10.1145/505863.505888.
  4. Adel Bouhoula & Florent Jacquemard (2008): Automated Induction with Constrained Tree Automata. In: Alessandro Armando, Peter Baumgartner & Gilles Dowek: Proceedings of the 4th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science 5195. Springer, pp. 539–554, doi:10.1007/978-3-540-71070-7_44.
  5. Stephan Falke & Deepak Kapur (2008): Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures. In: Andrei Voronkov: Proceedings of the 19th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 5117. Springer, pp. 94–109, doi:10.1007/978-3-540-70590-1_7.
  6. Stephan Falke & Deepak Kapur (2009): A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. In: Renate A. Schmidt: Proceedings of the 22nd International Conference on Automated Deduction, Lecture Notes in Computer Science 5663. Springer, pp. 277–293, doi:10.1007/978-3-642-02959-2_22.
  7. Stephan Falke & Deepak Kapur (2012): Rewriting Induction + Linear Arithmetic = Decision Procedure. In: Bernhard Gramlich, Dale Miller & Uli Sattler: Proceedings of the 6th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science 7364. Springer, pp. 241–255, doi:10.1007/978-3-642-31365-3_20.
  8. Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, René Thiemann & Harald Zankl (2008): Maximal Termination. In: Andrei Voronkov: Proceedings of the 19th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 5117. Springer, pp. 110–125, doi:10.1007/978-3-540-70590-1_8.
  9. Carsten Fuhs, Jürgen Giesl, Martin Plücker, Peter Schneider-Kamp & Stephan Falke (2009): Proving Termination of Integer Term Rewriting. In: Ralf Treinen: Proceedings of the 20th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science 5595. Springer, pp. 32–47, doi:10.1007/978-3-642-02348-4_3.
  10. Carsten Fuhs, Cynthia Kop & Naoki Nishida (2017): Verifying Procedural Programs via Constrained Rewriting Induction. ACM Transactions on Computational Logic 18(2), pp. 14:1–14:50, doi:10.1145/3060143.
  11. Yuki Furuichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari & Toshiki Sakabe (2008): Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems. IPSJ Transactions on Programming 1(2), pp. 100–121. In Japanese (a translated summary is available from http://www.trs.css.i.nagoya-u.ac.jp/crisys/).
  12. Jürgen Giesl (1997): Termination of Nested and Mutually Recursive Algorithms. Journal of Automated Reasoning 19(1), pp. 1–29, doi:10.1023/A:1005797629953.
  13. Jürgen Giesl, Peter Schneider-Kamp & René Thiemann (2006): AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. In: Ulrich Furbach & Natarajan Shankar: Proceedings of the 3rd International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science 4130. Springer, pp. 281–286, doi:10.1007/11814771_24.
  14. Jürgen Giesl, René Thiemann & Peter Schneider-Kamp (2005): The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. In: Franz Baader & Andrei Voronkov: Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science 3452. Springer, pp. 301–331, doi:10.1007/978-3-540-32275-7_21.
  15. Jürgen Giesl, René Thiemann, Peter Schneider-Kamp & Stephan Falke (2006): Mechanizing and Improving Dependency Pairs. Journal of Automated Reasoning 37(3), pp. 155–203, doi:10.1007/s10817-006-9057-7.
  16. Cynthia Kop (2013): Termination of LCTRSs (extended abstract). In: Proceedings of the 13th International Workshop on Termination, pp. 1–5. Available at http://www.imn.htwk-leipzig.de/WST2013/papers/paper_12.pdf.
  17. Cynthia Kop & Naoki Nishida (2013): Term Rewriting with Logical Constraints. In: Pascal Fontaine, Christophe Ringeissen & Renate A. Schmidt: Proceedings of the 9th International Symposium on Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence 8152, pp. 343–358, doi:10.1007/978-3-642-40885-4_24.
  18. Cynthia Kop & Naoki Nishida (2014): Automatic Constrained Rewriting Induction towards Verifying Procedural Programs. In: Jacques Garrigue: Proceedings of the 12th Asian Symposium on Programming Languages and Systems, Lecture Notes in Computer Science 8858, pp. 334–353, doi:10.1007/978-3-319-12736-1_18.
  19. Cynthia Kop & Naoki Nishida (2015): Constrained Term Rewriting tooL. In: Martin Davis, Ansgar Fehnker, Annabelle McIver & Andrei Voronkov: Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science 9450, pp. 549–557, doi:10.1007/978-3-662-48899-7_38.
  20. Salvador Lucas & José Meseguer (2014): 2D Dependency Pairs for Proving Operational Termination of CTRSs. In: Santiago Escobar: Proceedings of the 10th International Workshop on Rewriting Logic and Its Applications, Lecture Notes in Computer Science 8663. Springer, pp. 195–212, doi:10.1007/978-3-319-12904-4_11.
  21. Leonardo Mendonça de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: C. R. Ramakrishnan & Jakob Rehof: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 4963. Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  22. Enno Ohlebusch (2002): Advanced Topics in Term Rewriting. Springer, doi:10.1007/978-1-4757-3661-8.
  23. Tsubasa Sakata, Naoki Nishida & Toshiki Sakabe (2011): On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs. In: Herbert Kuchen: Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming, Lecture Notes in Computer Science 6816. Springer, pp. 138–155, doi:10.1007/978-3-642-22531-4_9.
  24. Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai & Keiichirou Kusakari (2009): Rewriting Induction for Constrained Term Rewriting Systems. IPSJ Transactions on Programming 2(2), pp. 80–96. In Japanese (a translated summary is available from http://www.trs.css.i.nagoya-u.ac.jp/crisys/).
  25. Yoshihito Toyama (1987): Confluent Term Rewriting Systems with Membership Conditions. In: Stéphane Kaplan & Jean-Pierre Jouannaud: Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems, Lecture Notes in Computer Science 308. Springer, pp. 228–241, doi:10.1007/3-540-19242-5_17.
  26. Hans Zantema (2003): Termination. In: Term Rewriting Systems, chapter 6, Cambridge Tracts in Theoretical Computer Science 55. Cambridge University Press, pp. 181–259, doi:10.1017/S1471068405222445.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org