@inproceedings(AEFGGLST08,
 author       = {Beatriz Alarc{\'{o}}n and Fabian Emmes and Carsten Fuhs and J{\"{u}}rgen Giesl and Ra{\'{u}}l Guti{\'{e}}rrez and Salvador Lucas and Schneider{-}Kamp, Peter and Ren{\'{e}} Thiemann},
 year         = {2008},
 title        = {Improving Context-Sensitive Dependency Pairs},
 editor       = {Iliano Cervesato and Helmut Veith and Andrei Voronkov},
 booktitle    = {Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
 series       = {Lecture Notes in Computer Science},
 volume       = {5330},
 publisher    = {Springer},
 pages        = {636--651},
 doi          = {10.1007/978-3-540-89439-1\_44},
)
@article(AG00,
 author       = {Thomas Arts and J{\"{u}}rgen Giesl},
 year         = {2000},
 title        = {Termination of term rewriting using dependency pairs},
 journal      = {Theoretical Computer Science},
 volume       = {236},
 number       = {1-2},
 pages        = {133--178},
 doi          = {10.1016/S0304-3975(99)00207-8},
)
@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},
)
@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(FGMSKTZ08,
 author       = {Carsten Fuhs and J{\"{u}}rgen Giesl and Aart Middeldorp and Schneider{-}Kamp, Peter and Ren{\'{e}} Thiemann and Harald Zankl},
 year         = {2008},
 title        = {Maximal Termination},
 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        = {110--125},
 doi          = {10.1007/978-3-540-70590-1\_8},
)
@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(Giesl97,
 author       = {J{\"{u}}rgen Giesl},
 year         = {1997},
 title        = {Termination of Nested and Mutually Recursive Algorithms},
 journal      = {Journal of Automated Reasoning},
 volume       = {19},
 number       = {1},
 pages        = {1--29},
 doi          = {10.1023/A:1005797629953},
)
@inproceedings(AProVE,
 author       = {J{\"u}rgen Giesl and Schneider-Kamp, Peter and Ren{\'e} Thiemann},
 year         = {2006},
 title        = {AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework},
 editor       = {Ulrich Furbach and Natarajan Shankar},
 booktitle    = {Proceedings of the 3rd International Joint Conference on Automated Reasoning},
 series       = {Lecture Notes in Computer Science},
 volume       = {4130},
 publisher    = {Springer},
 pages        = {281--286},
 doi          = {10.1007/11814771\_24},
)
@inproceedings(GTS04,
 author       = {J{\"{u}}rgen Giesl and Ren{\'{e}} Thiemann and Schneider-Kamp, Peter},
 year         = {2005},
 title        = {The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs},
 editor       = {Franz Baader and Andrei Voronkov},
 booktitle    = {Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning},
 series       = {Lecture Notes in Computer Science},
 volume       = {3452},
 publisher    = {Springer},
 pages        = {301--331},
 doi          = {10.1007/978-3-540-32275-7\_21},
)
@article(GTSF06,
 author       = {J{\"{u}}rgen Giesl and Ren{\'{e}} Thiemann and Schneider{-}Kamp, Peter and Stephan Falke},
 year         = {2006},
 title        = {Mechanizing and Improving Dependency Pairs},
 journal      = {Journal of Automated Reasoning},
 volume       = {37},
 number       = {3},
 pages        = {155--203},
 doi          = {10.1007/s10817-006-9057-7},
)
@inproceedings(Kop13,
 author       = {Cynthia Kop},
 year         = {2013},
 title        = {Termination of {LCTRSs} (extended abstract)},
 booktitle    = {Proceedings of the 13th International Workshop on Termination},
 pages        = {1--5},
 url          = {http://www.imn.htwk-leipzig.de/WST2013/papers/paper\_12.pdf},
)
@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 Artificial Intelligence},
 volume       = {8152},
 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},
 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},
 pages        = {549--557},
 doi          = {10.1007/978-3-662-48899-7\_38},
)
@inproceedings(LM14,
 author       = {Salvador Lucas and Jos{\'{e}} Meseguer},
 year         = {2014},
 title        = {{2D} Dependency Pairs for Proving Operational Termination of {CTRSs}},
 editor       = {Santiago Escobar},
 booktitle    = {Proceedings of the 10th International Workshop on Rewriting Logic and Its Applications},
 series       = {Lecture Notes in Computer Science},
 volume       = {8663},
 publisher    = {Springer},
 pages        = {195--212},
 doi          = {10.1007/978-3-319-12904-4\_11},
)
@inproceedings(z3,
 author       = {Leonardo Mendon{\c{c}}a de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3}: An Efficient {SMT} Solver},
 editor       = {C. R. Ramakrishnan and Jakob Rehof},
 booktitle    = {Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3\_24},
)
@book(Ohl02,
 author       = {Enno Ohlebusch},
 year         = {2002},
 title        = {Advanced Topics in Term Rewriting},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4757-3661-8},
)
@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(Toy87,
 author       = {Yoshihito Toyama},
 year         = {1987},
 title        = {Confluent Term Rewriting Systems with Membership Conditions},
 editor       = {St{\'e}phane Kaplan and Jean-Pierre Jouannaud},
 booktitle    = {Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems},
 series       = {Lecture Notes in Computer Science},
 volume       = {308},
 publisher    = {Springer},
 pages        = {228--241},
 doi          = {10.1007/3-540-19242-5\_17},
)
@incollection(Zan03,
 author       = {Hans Zantema},
 year         = {2003},
 title        = {Termination},
 booktitle    = {{Term Rewriting Systems}},
 chapter      = {6},
 series       = {Cambridge Tracts in Theoretical Computer Science},
 volume       = {55},
 publisher    = {Cambridge University Press},
 pages        = {181--259},
 doi          = {10.1017/S1471068405222445},
)