| 2026 | IJCAR | The ARI Infrastructure for Automated Confluence Analysis. | Nao Hirokawa, Aart Middeldorp, Teppei Saito, Ren Thiemann |
| 2026 | IJCAR | Unification of Deterministic Higher-Order Patterns. | Johannes Niederhauser, Aart Middeldorp |
| 2025 | CADE | The Computability Path Order for Beta-Eta-Normal Higher-Order Rewriting. | Johannes Niederhauser, Aart Middeldorp |
| 2025 | CPP | Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems. | Christina Kirk, Aart Middeldorp |
| 2025 | TACAS | Automated Analysis of Logically Constrained Rewrite Systems using crest. | Jonas Schpf, Aart Middeldorp |
| 2024 | IJCAR | Confluence of Logically Constrained Rewrite Systems Revisited. | Jonas Schpf, Fabian Mitterwallner, Aart Middeldorp |
| 2024 | LICS | Linear Termination is Undecidable. | Fabian Mitterwallner, Aart Middeldorp, Ren Thiemann |
| 2023 | CADE | Left-Linear Completion with AC Axioms. | Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp |
| 2023 | CADE | Confluence Criteria for Logically Constrained Rewrite Systems. | Jonas Schpf, Aart Middeldorp |
| 2023 | CPP | A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems. | Christina Kohl, Aart Middeldorp |
| 2023 | FSCD | Hydra Battles and AC Termination. | Nao Hirokawa, Aart Middeldorp |
| 2023 | ITP | Formalizing Almost Development Closed Critical Pairs (Short Paper). | Christina Kohl, Aart Middeldorp |
| 2022 | FSCD | Polynomial Termination Over ℕ Is Undecidable. | Fabian Mitterwallner, Aart Middeldorp |
| 2021 | CPP | A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems. | Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer |
| 2021 | TACAS | Certifying Proofs in the First-Order Theory of Rewriting. | Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer |
| 2020 | TACAS | Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting. | Alexander Lochmann, Aart Middeldorp |
| 2019 | CADE | Composing Proof Terms. | Christina Kohl, Aart Middeldorp |
| 2019 | CPP | A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL. | Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, Franziska Rapp |
| 2019 | TACAS | Confluence Competition 2019. | Aart Middeldorp, Julian Nagele, Kiraku Shintani |
| 2018 | CADE | Cops and CoCoWeb: Infrastructure for Confluence Tools. | Nao Hirokawa, Julian Nagele, Aart Middeldorp |
| 2018 | CADE | FORT 2.0. | Franziska Rapp, Aart Middeldorp |
| 2017 | CADE | CSI: New Evidence - A Progress Report. | Julian Nagele, Bertram Felgenhauer, Aart Middeldorp |
| 2017 | ICTAC | Constructing Cycles in the Simplex Method for DPLL(T). | Bertram Felgenhauer, Aart Middeldorp |
| 2016 | ITP | Certification of Classical Confluence Results for Left-Linear Term Rewrite Systems. | Julian Nagele, Aart Middeldorp |
| 2014 | FLOPS | AC-KBO Revisited. | Akihisa Yamada, Sarah Winkler, Nao Hirokawa, Aart Middeldorp |
| 2014 | ITP | A New and Formalized Proof of Abstract Completion. | Nao Hirokawa, Aart Middeldorp, Christian Sternagel |
| 2012 | LPAR | Matrix Interpretations for Polynomial Derivational Complexity of Rewrite Systems. | Aart Middeldorp |
| 2012 | LPAR | On the Domain and Dimension Hierarchy of Matrix Interpretations. | Friedrich Neurauter, Aart Middeldorp |
| 2012 | LPAR | Ordinals and Knuth-Bendix Orders. | Sarah Winkler, Harald Zankl, Aart Middeldorp |
| 2011 | CADE | AC Completion with Termination Tools. | Sarah Winkler, Aart Middeldorp |
| 2011 | CADE | CSI - A Confluence Tool. | Harald Zankl, Bertram Felgenhauer, Aart Middeldorp |
| 2010 | CADE | Decreasing Diagrams and Relative Termination. | Nao Hirokawa, Aart Middeldorp |
| 2010 | CADE | Monotonicity Criteria for Polynomial Interpretations over the Naturals. | Friedrich Neurauter, Aart Middeldorp, Harald Zankl |
| 2010 | CADE | Termination Tools in Ordered Completion. | Sarah Winkler, Aart Middeldorp |
| 2010 | LPAR | Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting. | Friedrich Neurauter, Harald Zankl, Aart Middeldorp |
| 2010 | LPAR | Satisfiability of Non-linear (Ir)rational Arithmetic. | Harald Zankl, Aart Middeldorp |
| 2010 | SOFSEM | Finding and Certifying Loops. | Harald Zankl, Christian Sternagel, Dieter Hofbauer, Aart Middeldorp |
| 2009 | CADE | Beyond Dependency Graphs. | Martin Korp, Aart Middeldorp |
| 2008 | AISC | Increasing Interpretations. | Harald Zankl, Aart Middeldorp |
| 2008 | CADE | Multi-completion with Termination Tools (System Description). | Haruhiko Sato, Sarah Winkler, Masahito Kurihara, Aart Middeldorp |
| 2008 | LATA | Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems. | Martin Korp, Aart Middeldorp |
| 2008 | LPAR | Uncurrying for Termination. | Nao Hirokawa, Aart Middeldorp, Harald Zankl |
| 2007 | CADE | Predictive Labeling with Dependency Pairs Using SAT. | Adam Koprowski, Aart Middeldorp |
| 2007 | SAT | SAT Solving for Termination Analysis with Polynomial Interpretations. | Carsten Fuhs, Jrgen Giesl, Aart Middeldorp, Peter Schneider-Kamp, Ren Thiemann, Harald Zankl |
| 2007 | SOFSEM | Constraints for Argument Filterings. | Harald Zankl, Nao Hirokawa, Aart Middeldorp |
| 2004 | AISC | Polynomial Interpretations with Negative Coefficients. | Nao Hirokawa, Aart Middeldorp |
| 2004 | PPDP | New completeness results for lazy conditional narrowing. | Mircea Marin, Aart Middeldorp |
| 2003 | CADE | Automating the Dependency Pair Method. | Nao Hirokawa, Aart Middeldorp |
| 2002 | DLT | Innermost Termination of Context-Sensitive Rewriting. | Jrgen Giesl, Aart Middeldorp |
| 2001 | CADE | Approximating Dependency Graphs Using Tree Automata Techniques. | Aart Middeldorp |
| 2001 | FLOPS | A Complete Selection Function for Lazy Conditional Narrowing. | Taro Suzuki, Aart Middeldorp |
| 2001 | FOSSACS | On the Modularity of Deciding Call-by-Need. | Irne Durand, Aart Middeldorp |
| 2000 | CADE | Eliminating Dummy Elimination. | Jrgen Giesl, Aart Middeldorp |
| 2000 | CSL | Equational Termination by Semantic Labelling. | Hitoshi Ohsaki, Aart Middeldorp, Jrgen Giesl |
| 1999 | CSL | Term Rewriting. | Aart Middeldorp |
| 1997 | CADE | Decidable Call by Need Computations in term Rewriting (Extended Abstract). | Irne Durand, Aart Middeldorp |
| 1997 | LFCS | Type Introduction for Equational Rewriting. | Hitoshi Ohsaki, Aart Middeldorp |
| 1997 | POPL | Call by Need Computations to Root-Stable Form. | Aart Middeldorp |
| 1996 | CADE | Transforming Termination by Self-Labelling. | Aart Middeldorp, Hitoshi Ohsaki, Hans Zantema |
| 1996 | CSL | Relative Undecidability in Term Rewriting. | Alfons Geser, Aart Middeldorp, Enno Ohlebusch, Hans Zantema |
| 1994 | CADE | Simple Termination Revisited. | Aart Middeldorp, Hans Zantema |
| 1989 | LICS | A Sufficient Condition for the Termination of the Direct Sum of Term Rewriting Systems | Aart Middeldorp |