| 2026 | IJCAR | The ARI Infrastructure for Automated Confluence Analysis. | Nao Hirokawa, Aart Middeldorp, Teppei Saito, Ren Thiemann |
| 2026 | IJCAR | An Applicative Multiset Path Order. | Nao Hirokawa, Teppei Saito, Teppei Tanaka, Wataru Yachi |
| 2025 | CADE | Lexicographic Combination of Reduction Pairs. | Teppei Saito, Nao Hirokawa |
| 2024 | CPP | Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs. | Nao Hirokawa, Dohan Kim, Kiraku Shintani, Ren Thiemann |
| 2024 | FSCD | Simulating Dependency Pairs by Semantic Labeling. | Teppei Saito, Nao Hirokawa |
| 2023 | CADE | Left-Linear Completion with AC Axioms. | Johannes Niederhauser, Nao Hirokawa, Aart Middeldorp |
| 2023 | FSCD | Hydra Battles and AC Termination. | Nao Hirokawa, Aart Middeldorp |
| 2022 | FSCD | Compositional Confluence Criteria. | Kiraku Shintani, Nao Hirokawa |
| 2021 | FSCD | Completion and Reduction Orders (Invited Talk). | Nao Hirokawa |
| 2019 | CADE | Confluence by Critical Pair Analysis Revisited. | Nao Hirokawa, Julian Nagele, Vincent van Oostrom, Michio Oyamaguchi |
| 2018 | CADE | Cops and CoCoWeb: Infrastructure for Confluence Tools. | Nao Hirokawa, Julian Nagele, Aart Middeldorp |
| 2015 | CADE | Confluence Competition 2015. | Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, Harald Zankl |
| 2015 | CADE | CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems. | Kiraku Shintani, Nao Hirokawa |
| 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 | Confluence of Non-Left-Linear TRSs via Relative Termination. | Dominik Klein, Nao Hirokawa |
| 2010 | CADE | Decreasing Diagrams and Relative Termination. | Nao Hirokawa, Aart Middeldorp |
| 2008 | CADE | Automated Complexity Analysis Based on the Dependency Pair Method. | Nao Hirokawa, Georg Moser |
| 2008 | LPAR | Complexity, Graphs, and the Dependency Pair Method. | Nao Hirokawa, Georg Moser |
| 2008 | LPAR | Uncurrying for Termination. | Nao Hirokawa, Aart Middeldorp, 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 |
| 2003 | CADE | Automating the Dependency Pair Method. | Nao Hirokawa, Aart Middeldorp |