SAT Techniques for Lexicographic Path Orders - Harald Zankl (CoRR, 2006)

Implementing RPO and POLO using SAT. - Peter Schneider-Kamp; Carsten Fuhs; René Thiemann; Jürgen Giesl; Elena Annov; Michael Codish; Aart Middeldorp; Harald Zankl (Deduction and Decision Procedures, 2007)

Satisfying KBO Constraints. - Harald Zankl; Aart Middeldorp (RTA, 2007)

SAT Solving for Termination Analysis with Polynomial Interpretations. - Carsten Fuhs; Jürgen Giesl; Aart Middeldorp; Peter Schneider-Kamp; René Thiemann; Harald Zankl (SAT, 2007)

Constraints for Argument Filterings. - Harald Zankl; Nao Hirokawa; Aart Middeldorp (SOFSEM (1), 2007)

Uncurrying for Termination. - Nao Hirokawa; Aart Middeldorp; Harald Zankl (LPAR, 2008)

Maximal Termination. - Carsten Fuhs; Jürgen Giesl; Aart Middeldorp; Peter Schneider-Kamp; René Thiemann; Harald Zankl (RTA, 2008)

Transforming SAT into Termination of Rewriting. - Harald Zankl; Christian Sternagel; Aart Middeldorp (WFLP, 2008)

Tyrolean Termination Tool 2. - Martin Korp; Christian Sternagel; Harald Zankl; Aart Middeldorp (RTA, 2009)

Increasing interpretations. - Harald Zankl; Aart Middeldorp (Ann. Math. Artif. Intell., 2009)

KBO Orientability. - Harald Zankl; Nao Hirokawa; Aart Middeldorp (J. Autom. Reason., 2009)

Monotonicity Criteria for Polynomial Interpretations over the Naturals. - Friedrich Neurauter; Aart Middeldorp; Harald Zankl (IJCAR, 2010)

Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting. - Friedrich Neurauter; Harald Zankl; Aart Middeldorp (LPAR (Yogyakarta), 2010)

On Implementing Modular Complexity Analysis. - Harald Zankl; Martin Korp (IWIL@LPAR, 2010)

Satisfiability of Non-linear (Ir)rational Arithmetic. - Harald Zankl; Aart Middeldorp (LPAR (Dakar), 2010)

Modular Complexity Analysis via Relative Complexity. - Harald Zankl; Martin Korp (RTA, 2010)

Finding and Certifying Loops. - Harald Zankl; Christian Sternagel; Dieter Hofbauer; Aart Middeldorp (SOFSEM, 2010)

Uncurrying for Innermost Termination and Derivational Complexity - Harald Zankl; Nao Hirokawa; Aart Middeldorp (HOR, 2010)

CSI - A Confluence Tool. - Harald Zankl; Bertram Felgenhauer; Aart Middeldorp (CADE, 2011)

Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems. - Aart Middeldorp; Georg Moser; Friedrich Neurauter; Johannes Waldmann; Harald Zankl (CAI, 2011)

Layer Systems for Proving Confluence. - Bertram Felgenhauer; Harald Zankl; Aart Middeldorp (FSTTCS, 2011)

KBCV - Knuth-Bendix Completion Visualizer. - Thomas Sternagel; Harald Zankl (IJCAR, 2012)

Ordinals and Knuth-Bendix Orders. - Sarah Winkler; Harald Zankl; Aart Middeldorp (LPAR, 2012)

CeTA - A Tool for Certified Termination Analysis - Christian Sternagel; René Thiemann; Sarah Winkler; Harald Zankl (CoRR, 2012)

Recording Completion for Finding and Certifying Proofs in Equational Logic - Thomas Sternagel; René Thiemann; Harald Zankl; Christian Sternagel (CoRR, 2012)

Beyond Peano Arithmetic - Automatically Proving Termination of the Goodstein Sequence. - Sarah Winkler; Harald Zankl; Aart Middeldorp (RTA, 2013)

Confluence by Decreasing Diagrams - Formalized. - Harald Zankl (RTA, 2013)

Decreasing Diagrams. - Harald Zankl (Arch. Formal Proofs, 2013)

Uncurrying for Termination and Complexity. - Nao Hirokawa; Aart Middeldorp; Harald Zankl (J. Autom. Reason., 2013)

Modular Complexity Analysis for Term Rewriting. - Harald Zankl; Martin Korp (Log. Methods Comput. Sci., 2014)

Confluence Competition 2015. - Takahito Aoto 001; Nao Hirokawa; Julian Nagele; Naoki Nishida 001; Harald Zankl (CADE, 2015)

Recording Completion for Certificates in Equational Reasoning. - Thomas Sternagel; Sarah Winkler; Harald Zankl (CPP, 2015)

Certified Rule Labeling. - Julian Nagele; Harald Zankl (RTA, 2015)

Labelings for Decreasing Diagrams. - Harald Zankl; Bertram Felgenhauer; Aart Middeldorp (J. Autom. Reason., 2015)

Beyond polynomials and Peano arithmetic - automation of elementary and ordinal interpretations. - Harald Zankl; Sarah Winkler; Aart Middeldorp (J. Symb. Comput., 2015)

Layer Systems for Proving Confluence. - Bertram Felgenhauer; Aart Middeldorp; Harald Zankl; Vincent van Oostrom (ACM Trans. Comput. Log., 2015)

Certifying Confluence Proofs via Relative Termination and Rule Labeling. - Julian Nagele; Bertram Felgenhauer; Harald Zankl (Log. Methods Comput. Sci., 2017)

Confluence Competition 2018. - Takahito Aoto 001; Makoto Hamana; Nao Hirokawa; Aart Middeldorp; Julian Nagele; Naoki Nishida 001; Kiraku Shintani; Harald Zankl (FSCD, 2018)