@book(BN98,
 author       = {Franz Baader and Tobias Nipkow},
 year         = {1998},
 title        = {Term Rewriting and All That},
 publisher    = {Cambridge University Press},
 doi          = {10.1145/505863.505888},
)
@inproceedings(BJ08,
 author       = {Adel Bouhoula and Florent Jacquemard},
 year         = {2008},
 title        = {Automated Induction with Constrained Tree Automata},
 editor       = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
 booktitle    = {Proceedings of the 4th International Joint Conference on Automated Reasoning},
 series       = {Lecture Notes in Computer Science},
 volume       = {5195},
 publisher    = {Springer},
 pages        = {539--554},
 doi          = {10.1007/978-3-540-71070-7\_44},
)
@book(BM07,
 author       = {Aaron R. Bradley and Zohar Manna},
 year         = {2007},
 title        = {The Calculus of Computation: Decision Procedures with Applications to Verification},
 publisher    = {Springer},
 doi          = {10.1007/978-3-540-74113-8},
)
@inproceedings(FK08,
 author       = {Stephan Falke and Deepak Kapur},
 year         = {2008},
 title        = {Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures},
 editor       = {Andrei Voronkov},
 booktitle    = {Proceedings of the 19th International Conference on Rewriting Techniques and Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {5117},
 publisher    = {Springer},
 pages        = {94--109},
 doi          = {10.1007/978-3-540-70590-1\_7},
)
@inproceedings(FK09,
 author       = {Stephan Falke and Deepak Kapur},
 year         = {2009},
 title        = {A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs},
 editor       = {Renate A. Schmidt},
 booktitle    = {Proceedings of the 22nd International Conference on Automated Deduction},
 series       = {Lecture Notes in Computer Science},
 volume       = {5663},
 publisher    = {Springer},
 pages        = {277--293},
 doi          = {10.1007/978-3-642-02959-2\_22},
)
@inproceedings(FK12,
 author       = {Stephan Falke and Deepak Kapur},
 year         = {2012},
 title        = {Rewriting Induction + Linear Arithmetic = Decision Procedure},
 editor       = {Bernhard Gramlich and Dale Miller and Uli Sattler},
 booktitle    = {Proceedings of the 6th International Joint Conference on Automated Reasoning},
 series       = {Lecture Notes in Computer Science},
 volume       = {7364},
 publisher    = {Springer},
 pages        = {241--255},
 doi          = {10.1007/978-3-642-31365-3\_20},
)
@inproceedings(FGPSF09,
 author       = {Carsten Fuhs and J{\"{u}}rgen Giesl and Martin Pl{\"{u}}cker and Schneider{-}Kamp, Peter and Stephan Falke},
 year         = {2009},
 title        = {Proving Termination of Integer Term Rewriting},
 editor       = {Ralf Treinen},
 booktitle    = {Proceedings of the 20th International Conference on Rewriting Techniques and Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {5595},
 publisher    = {Springer},
 pages        = {32--47},
 doi          = {10.1007/978-3-642-02348-4\_3},
)
@article(FKN17tocl,
 author       = {Carsten Fuhs and Cynthia Kop and Naoki Nishida},
 year         = {2017},
 title        = {Verifying Procedural Programs via Constrained Rewriting Induction},
 journal      = {ACM Transactions on Computational Logic},
 volume       = {18},
 number       = {2},
 pages        = {14:1--14:50},
 doi          = {10.1145/3060143},
)
@article(FNSKS08b,
 author       = {Yuki Furuichi and Naoki Nishida and Masahiko Sakai and Keiichirou Kusakari and Toshiki Sakabe},
 year         = {2008},
 title        = {Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems},
 journal      = {IPSJ Transactions on Programming},
 volume       = {1},
 number       = {2},
 pages        = {100--121},
 note         = {In Japanese (a translated summary is available from \url{http://www.trs.css.i.nagoya-u.ac.jp/crisys/})},
)
@article(Hue82,
 author       = {G\'erard Huet and Jean-Marie Hullot},
 year         = {1982},
 title        = {Proof by Induction in Equational Theories with Constructors},
 journal      = {Journal of Computer and System Science},
 volume       = {25},
 number       = {2},
 pages        = {239--266},
 doi          = {10.1016/0022-0000(82)90006-X},
)
@inproceedings(KN13frocos,
 author       = {Cynthia Kop and Naoki Nishida},
 year         = {2013},
 title        = {Term Rewriting with Logical Constraints},
 editor       = {Pascal Fontaine and Christophe Ringeissen and Renate A. Schmidt},
 booktitle    = {Proceedings of the 9th International Symposium on Frontiers of Combining Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {8152},
 publisher    = {Springer},
 pages        = {343--358},
 doi          = {10.1007/978-3-642-40885-4\_24},
)
@inproceedings(KN14aplas,
 author       = {Cynthia Kop and Naoki Nishida},
 year         = {2014},
 title        = {Automatic Constrained Rewriting Induction towards Verifying Procedural Programs},
 editor       = {Jacques Garrigue},
 booktitle    = {Proceedings of the 12th Asian Symposium on Programming Languages and Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {8858},
 publisher    = {Springer},
 pages        = {334--353},
 doi          = {10.1007/978-3-319-12736-1\_18},
)
@inproceedings(KN15lpar,
 author       = {Cynthia Kop and Naoki Nishida},
 year         = {2015},
 title        = {Constrained Term Rewriting tooL},
 editor       = {Martin Davis and Ansgar Fehnker and Annabelle McIver and Andrei Voronkov},
 booktitle    = {Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
 series       = {Lecture Notes in Computer Science},
 volume       = {9450},
 publisher    = {Springer},
 pages        = {549--557},
 doi          = {10.1007/978-3-662-48899-7\_38},
)
@inproceedings(Mus80,
 author       = {David R. Musser},
 year         = {1980},
 title        = {On Proving Inductive Properties of Abstract Data Types},
 editor       = {Paul W. Abrahams and Richard J. Lipton and Stephen R. Bourne},
 booktitle    = {Proceedings of the 7th ACM Symposium on Principles of Programming Languages},
 pages        = {154--162},
 doi          = {10.1145/567446.567461},
)
@inproceedings(NK14wst,
 author       = {Naoki Nishida and Takumi Kataoka},
 year         = {2014},
 title        = {On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants},
 editor       = {Carsten Fuhs},
 booktitle    = {Proceedings of the 14th International Workshop on Termination},
 pages        = {1--5},
)
@book(Ohl02,
 author       = {Enno Ohlebusch},
 year         = {2002},
 title        = {Advanced Topics in Term Rewriting},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4757-3661-8},
)
@inproceedings(Red90,
 author       = {Uday S. Reddy},
 year         = {1990},
 title        = {Term Rewriting Induction},
 editor       = {Mark E. Stickel},
 booktitle    = {Proceedings of the 10th International Conference on Automated Deduction},
 series       = {Lecture Notes in Computer Science},
 volume       = {449},
 publisher    = {Springer},
 pages        = {162--177},
 doi          = {10.1007/3-540-52885-7\_86},
)
@book(Rey98,
 author       = {John C. Reynolds},
 year         = {1998},
 title        = {Theories of Programming Languages},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511626364},
)
@inproceedings(SNS11,
 author       = {Tsubasa Sakata and Naoki Nishida and Toshiki Sakabe},
 year         = {2011},
 title        = {On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs},
 editor       = {Herbert Kuchen},
 booktitle    = {Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming},
 series       = {Lecture Notes in Computer Science},
 volume       = {6816},
 publisher    = {Springer},
 pages        = {138--155},
 doi          = {10.1007/978-3-642-22531-4\_9},
)
@article(SNSSK09,
 author       = {Tsubasa Sakata and Naoki Nishida and Toshiki Sakabe and Masahiko Sakai and Keiichirou Kusakari},
 year         = {2009},
 title        = {Rewriting Induction for Constrained Term Rewriting Systems},
 journal      = {IPSJ Transactions on Programming},
 volume       = {2},
 number       = {2},
 pages        = {80--96},
 note         = {In Japanese (a translated summary is available from \url{http://www.trs.css.i.nagoya-u.ac.jp/crisys/})},
)
@inproceedings(Vid12,
 author       = {Germ{\'{a}}n Vidal},
 year         = {2012},
 title        = {Closed Symbolic Execution for Verifying Program Termination},
 booktitle    = {Proceedings of the 12th {IEEE} International Working Conference on Source Code Analysis and Manipulation},
 publisher    = {{IEEE} Computer Society},
 pages        = {34--43},
 doi          = {10.1109/SCAM.2012.13},
)