@conference(Aoto13,
 author       = "Takahito Aoto",
 year         = "2013",
 title        = "Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering",
 booktitle    = "Proc.\ FroCoS",
 series       = "LNCS",
 volume       = "8152",
 publisher    = "Springer",
 pages        = "311--326",
 doi          = "10.1007/978-3-642-40885-4\_22",
)
@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       = "\unhbox \voidb@x \hbox {1-2}",
 pages        = "133--178",
 doi          = "10.1016/S0304-3975(99)00207-8",
)
@conference(tct,
 author       = "Martin Avanzini and Georg Moser",
 year         = "2013",
 title        = "{Tyrolean Complexity Tool}: Features and Usage",
 booktitle    = "Proc.\ RTA",
 series       = "LIPIcs",
 volume       = "21",
 publisher    = "Dagstuhl",
 pages        = "71--80",
 doi          = "10.4230/LIPIcs.RTA.2013.71",
)
@article(color,
 author       = "Fr{\'e}d{\'e}ric Blanqui and Adam Koprowski",
 year         = "2011",
 title        = "{\textsf {CoLoR}\xspace }: a {Coq} library on well-founded rewrite relations and its application on the automated verification of termination certificates",
 journal      = "Mathematical Structures in Computer Science",
 volume       = "21",
 number       = "4",
 pages        = "827--859",
 doi          = "10.1017/S0960129511000120",
)
@conference(CFGSK10,
 author       = "Michael Codish and Carsten Fuhs and J{\"u}rgen Giesl and Peter Schneider-Kamp",
 year         = "2010",
 title        = "Lazy Abstraction for Size-Change Termination",
 booktitle    = "Proc.\ LPAR",
 series       = "LNCS",
 volume       = "6397",
 publisher    = "Springer",
 pages        = "217--232",
 doi          = "10.1007/978-3-642-16242-8\_16",
)
@conference(a3pat-cime,
 author       = "{\'E}velyne Contejean and Pierre Courtieu and Julien Forest and Olivier Pons and Xavier Urbain",
 year         = "2011",
 title        = "Automated Certified Proofs with {\textsf {C\kern -0.1ex\textsl {i}ME}\xspace }3",
 booktitle    = "Proc.\ RTA",
 series       = "LIPIcs",
 volume       = "10",
 publisher    = "Dagstuhl",
 pages        = "21--30",
 doi          = "10.4230/LIPIcs.RTA.2011.21",
)
@article(D87,
 author       = "Nachum Dershowitz",
 year         = "1987",
 title        = "Termination of Rewriting",
 journal      = "Journal of Symbolic Computation",
 volume       = "3",
 number       = "\unhbox \voidb@x \hbox {1-2}",
 pages        = "69--116",
 doi          = "10.1016/S0747-7171(87)80022-6",
)
@conference(EEG12,
 author       = "Fabian Emmes and Tim Enger and J{\"u}rgen Giesl",
 year         = "2012",
 title        = "Proving Non-Looping Non-Termination Automatically",
 booktitle    = "Proc.\ IJCAR",
 series       = "LNCS",
 volume       = "7364",
 publisher    = "Springer",
 pages        = "225--240",
 doi          = "10.1007/978-3-642-31365-3\_19",
)
@article(EWZ08,
 author       = "J{\"o}rg Endrullis and Johannes Waldmann and Hans Zantema",
 year         = "2008",
 title        = "Matrix Interpretations for Proving Termination of Term Rewriting",
 journal      = "Journal of Automated Reasoning",
 volume       = "40",
 number       = "\unhbox \voidb@x \hbox {2-3}",
 pages        = "195--220",
 doi          = "10.1007/s10817-007-9087-9",
)
@conference(FT14,
 author       = "Bertram Felgenhauer and Ren{\'e} Thiemann",
 year         = "2014",
 title        = "Reachability Analysis with State-Compatible Automata",
 booktitle    = "Proc.\ LATA",
 series       = "LNCS",
 volume       = "8370",
 publisher    = "Springer",
 pages        = "347--359",
 doi          = "10.1007/978-3-319-04921-2\_28",
)
@article(matchbounds,
 author       = "Alfons Geser and Dieter Hofbauer and Johannes Waldmann and Hans Zantema",
 year         = "2007",
 title        = "On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems",
 journal      = "Information and Computation",
 volume       = "205",
 number       = "4",
 pages        = "512--534",
 doi          = "10.1007/978-3-540-32033-3\_26",
)
@conference(aprove,
 author       = "J\"urgen Giesl and Marc Brockschmidt and Fabian Emmes and Florian Frohn and Carsten Fuhs and Carsten Otto and Martin Pl\"ucker and Peter Schneider-Kamp and Thomas Str\"oder and Steffi Swiderski and Ren\'e Thiemann",
 year         = "2014",
 title        = "Proving Termination of Programs Automatically with {\textsf {AProVE}\xspace }",
 booktitle    = "Proc.\ IJCAR",
 series       = "LNAI",
 volume       = "8562",
 publisher    = "Springer",
 pages        = "184--191",
 doi          = "10.1007/978-3-319-08587-6\_13",
)
@article(dp-framework,
 author       = "J{\"u}rgen Giesl and Ren{\'e} Thiemann and Peter Schneider-Kamp 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",
)
@article(G95,
 author       = "Bernhard Gramlich",
 year         = "1995",
 title        = "Abstract Relations between Restricted Termination and Confluence Properties of Rewrite Systems",
 journal      = "Fundamenta Informaticae",
 volume       = "24",
 number       = "\unhbox \voidb@x \hbox {1-2}",
 pages        = "3--23",
 doi          = "10.3233/FI-1995-24121",
)
@article(HM07,
 author       = "Nao Hirokawa and Aart Middeldorp",
 year         = "2007",
 title        = "Tyrolean {Termination} {Tool}: Techniques and Features",
 journal      = "Information and Computation",
 volume       = "205",
 number       = "4",
 pages        = "474--511",
 doi          = "10.1016/j.ic.2006.08.010",
)
@article(UncurryHMZ,
 author       = "Nao Hirokawa and Aart Middeldorp and Harald Zankl",
 year         = "2013",
 title        = "Uncurrying for Termination and Complexity",
 journal      = "Journal of Automated Reasoning",
 volume       = "50",
 number       = "3",
 pages        = "279--315",
 doi          = "10.1007/s10817-012-9248-3",
)
@incollection(KB70,
 author       = "Donald E. Knuth and Peter B. Bendix",
 year         = "1970",
 title        = "Simple Word Problems in Universal Algebras",
 booktitle    = "Computational Problems in Abstract Algebra",
 pages        = "263--297",
 doi          = "10.1016/B978-0-08-012975-4.50028-X",
)
@conference(arctic,
 author       = "Adam Koprowski and Johannes Waldmann",
 year         = "2008",
 title        = "Arctic Termination \ldots \ Below Zero",
 booktitle    = "Proc.\ RTA",
 series       = "LNCS",
 volume       = "5117",
 publisher    = "Springer",
 pages        = "202--216",
 doi          = "10.1007/978-3-540-70590-1\_14",
)
@conference(ttt2,
 author       = "Martin Korp and Christian Sternagel and Harald Zankl and Aart Middeldorp",
 year         = "2009",
 title        = "{Tyrolean Termination Tool 2}",
 booktitle    = "Proc.\ RTA",
 series       = "LNCS",
 volume       = "5595",
 publisher    = "Springer",
 pages        = "295--304",
 doi          = "10.1007/978-3-642-02348-4\_21",
)
@techreport(L79,
 author       = "Dallas Lankford",
 year         = "1979",
 title        = "On Proving Term Rewriting Systems are {N}oetherian",
 type         = "Technical Report",
 number       = "MTP-3",
 institution  = "Louisiana Technical University",
 address      = "Ruston, LA, USA",
)
@conference(LJBA01,
 author       = "Chin Soon Lee and Neil D. Jones and Amir M. Ben-Amram",
 year         = "2001",
 title        = "The Size-Change Principle for Program Termination",
 booktitle    = "Proc.\ POPL",
 publisher    = "ACM New York, NY, USA",
 pages        = "81--92",
 doi          = "10.1145/373243.360210",
)
@article(rational,
 author       = "Salvador Lucas",
 year         = "2005",
 title        = "Polynomials over the reals in proofs of termination: From theory to practice",
 journal      = "RAIRO -- Theoretical Informatics and Applications",
 volume       = "39",
 number       = "3",
 pages        = "547--586",
 doi          = "10.1051/ita:2005029",
)
@conference(root-labeling,
 author       = "Christian Sternagel and Aart Middeldorp",
 year         = "2008",
 title        = "Root-{L}abeling",
 booktitle    = "Proc.\ RTA",
 series       = "LNCS",
 volume       = "5117",
 publisher    = "Springer",
 pages        = "336--350",
 doi          = "10.1007/978-3-540-70590-1\_23",
)
@conference(UncurryST,
 author       = "Christian Sternagel and Ren{\'e} Thiemann",
 year         = "2011",
 title        = "Generalized and Formalized Uncurrying",
 booktitle    = "Proc.\ FroCoS",
 series       = "LNAI",
 volume       = "6989",
 publisher    = "Springer",
 pages        = "243--258",
 doi          = "10.1007/978-3-642-24364-6\_17",
)
@conference(kbcv,
 author       = "Thomas Sternagel and Harald Zankl",
 year         = "2012",
 title        = "{KBCV} -- {Knuth-Bendix} Completion Visualizer",
 booktitle    = "Proc.\ IJCAR",
 series       = "LNCS",
 volume       = "7364",
 publisher    = "Springer",
 pages        = "530--536",
 doi          = "10.1007/978-3-642-31365-3\_41",
)
@article(AAECC05,
 author       = "Ren{\'e} Thiemann and J{\"u}rgen Giesl",
 year         = "2005",
 title        = "The size-change principle and dependency pairs for termination of term rewriting",
 journal      = "Applicable Algebra in Engineering, Communication and Computing",
 volume       = "16",
 number       = "4",
 pages        = "229--270",
 doi          = "10.1007/s00200-005-0179-7",
)
@conference(ceta-tphols,
 author       = "Ren{\'e} Thiemann and Christian Sternagel",
 year         = "2009",
 title        = "Certification of Termination Proofs using {\textsf {C\kern -0.2exe\kern -0.5exT\kern -0.5exA}\xspace }",
 booktitle    = "Proc.\ TPHOLs",
 series       = "LNCS",
 volume       = "5674",
 publisher    = "Springer",
 pages        = "452--468",
 doi          = "10.1007/978-3-642-03359-9\_31",
)
@conference(U01,
 author       = "Xavier Urbain",
 year         = "2001",
 title        = "Automated incremental termination proofs for hierarchically defined term rewriting systems",
 booktitle    = "Proc.\ IJCAR",
 series       = "LNAI",
 volume       = "2083",
 publisher    = "Springer",
 pages        = "485--498",
 doi          = "10.1007/3-540-45744-5\_42",
)
@conference(matchbox,
 author       = "Johannes Waldmann",
 year         = "2004",
 title        = "{\textsf {Matchbox}\xspace }: A Tool for Match-Bounded String Rewriting",
 booktitle    = "Proc.\ RTA",
 series       = "LNCS",
 volume       = "3091",
 publisher    = "Springer",
 pages        = "85--94",
 doi          = "10.1007/978-3-540-25979-4\_6",
)
@article(mkbtt,
 author       = "Sarah Winkler and Haruhiko Sato and Aart Middeldorp and Masahito Kurihara",
 year         = "2013",
 title        = "Multi-Completion with Termination Tools",
 journal      = "Journal of Automated Reasoning",
 volume       = "50",
 number       = "3",
 pages        = "317--354",
 doi          = "10.1007/s10817-012-9249-2",
)
@conference(csi,
 author       = "Harald Zankl and Bertram Felgenhauer and Aart Middeldorp",
 year         = "2011",
 title        = "{CSI -- A Confluence Tool}",
 booktitle    = "Proc.\ CADE",
 series       = "LNAI",
 volume       = "6803",
 publisher    = "Springer",
 pages        = "499--505",
 doi          = "10.1007/978-3-642-22438-6\_38",
)
@article(cat,
 author       = "Harald Zankl and Martin Korp",
 year         = "2014",
 title        = "Modular Complexity Analysis for Term Rewriting",
 journal      = "Logical Methods in Computer Science",
 volume       = "10",
 number       = "\unhbox \voidb@x \hbox {1:19}",
 pages        = "1--33",
 doi          = "10.2168/LMCS-10(1:19)2014",
)
@article(Z95,
 author       = "Hans Zantema",
 year         = "1995",
 title        = "Termination of Term Rewriting by Semantic Labelling",
 journal      = "Fundamenta Informaticae",
 volume       = "24",
 number       = "\unhbox \voidb@x \hbox {1-2}",
 pages        = "89--105",
 doi          = "10.3233/FI-1995-24124",
)