@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(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(FKS11,
 author       = {Stephan Falke and Deepak Kapur and Carsten Sinz},
 year         = {2011},
 title        = {Termination Analysis of {C} Programs Using Compiler Intermediate Languages},
 editor       = {Schmidt{-}Schau{\ss}, Manfred},
 booktitle    = {Proceedings of the 22nd International Conference on Rewriting Techniques and Applications},
 series       = {LIPIcs},
 volume       = {10},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum f\"ur Informatik},
 pages        = {41--50},
 doi          = {10.4230/LIPIcs.RTA.2011.41},
)
@book(Fer14,
 author       = {Maribel Fern{\'{a}}ndez},
 year         = {2014},
 title        = {Programming Languages and Operational Semantics -- {A} Concise Overview},
 series       = {Undergraduate Topics in Computer Science},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4471-6368-8},
)
@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/})},
)
@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(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},
)
@article(NNKSS11,
 author       = {Naoki Nakabayashi and Naoki Nishida and Keiichirou Kusakari and Toshiki Sakabe and Masahiko Sakai},
 year         = {2011},
 title        = {Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems},
 journal      = {Computer Software},
 volume       = {28},
 number       = {1},
 pages        = {173--189},
 note         = {In Japanese (a translated summary is available from \url{http://www.trs.css.i.nagoya-u.ac.jp/crisys/})},
)
@book(Ohl02,
 author       = {Enno Ohlebusch},
 year         = {2002},
 title        = {Advanced Topics in Term Rewriting},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4757-3661-8},
)
@inproceedings(Otto10,
 author       = {Carsten Otto and Marc Brockschmidt and Christian von Essen and J{\"u}rgen Giesl},
 year         = {2010},
 title        = {Automated termination analysis of {Java} bytecode by term rewriting},
 editor       = {Christopher Lynch},
 booktitle    = {Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
 series       = {LIPIcs},
 volume       = {6},
 publisher    = {Schloss Dagstuhl--Leibniz-Zentrum f\"ur Informatik},
 pages        = {259--276},
 doi          = {10.4230/LIPIcs.RTA.2010.259},
)
@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},
)
@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/})},
)