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.
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.
Franz Baader & Tobias Nipkow (1998):
Term Rewriting and All That.
Cambridge University Press,
doi:10.1145/505863.505888.
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.
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.
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.
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.
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.
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.
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.
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/).
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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/).
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.
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.