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.
Aaron R. Bradley & Zohar Manna (2007):
The Calculus of Computation: Decision Procedures with Applications to Verification.
Springer,
doi:10.1007/978-3-540-74113-8.
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, 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/).
Gérard Huet & Jean-Marie Hullot (1982):
Proof by Induction in Equational Theories with Constructors.
Journal of Computer and System Science 25(2),
pp. 239–266,
doi:10.1016/0022-0000(82)90006-X.
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 Computer Science 8152.
Springer,
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.
Springer,
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.
Springer,
pp. 549–557,
doi:10.1007/978-3-662-48899-7_38.
David R. Musser (1980):
On Proving Inductive Properties of Abstract Data Types.
In: Paul W. Abrahams, Richard J. Lipton & Stephen R. Bourne: Proceedings of the 7th ACM Symposium on Principles of Programming Languages,
pp. 154–162,
doi:10.1145/567446.567461.
Naoki Nishida & Takumi Kataoka (2014):
On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants.
In: Carsten Fuhs: Proceedings of the 14th International Workshop on Termination,
pp. 1–5.
Uday S. Reddy (1990):
Term Rewriting Induction.
In: Mark E. Stickel: Proceedings of the 10th International Conference on Automated Deduction,
Lecture Notes in Computer Science 449.
Springer,
pp. 162–177,
doi:10.1007/3-540-52885-7_86.
John C. Reynolds (1998):
Theories of Programming Languages.
Cambridge University Press,
doi:10.1017/CBO9780511626364.
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/).
Germán Vidal (2012):
Closed Symbolic Execution for Verifying Program Termination.
In: Proceedings of the 12th IEEE International Working Conference on Source Code Analysis and Manipulation.
IEEE Computer Society,
pp. 34–43,
doi:10.1109/SCAM.2012.13.