| 2026 | FSCD | Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification. | Misaki Kojima, Naoki Nishida |
| 2025 | LOPSTR | Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms. | Kanta Takahata, Jonas Schpf, Naoki Nishida, Takahito Aoto |
| 2025 | PPDP | Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations. | Kanta Takahata, Jonas Schpf, Naoki Nishida, Takahito Aoto |
| 2024 | FSCD | Equational Theories and Validity for Logically Constrained Term Rewriting. | Takahito Aoto, Naoki Nishida, Jonas Schpf |
| 2023 | PADL | From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting. | Misaki Kojima, Naoki Nishida |
| 2022 | FLOPS | On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs. | Shujun Zhang, Naoki Nishida |
| 2020 | RC | ReverCSP: Time-Travelling in CSP Computations. | Carlos Galindo, Naoki Nishida, Josep Silva, Salvador Tamarit |
| 2019 | AVSS | Exemplar-Based Pseudo-Viewpoint Rotation for White-Cane User Recognition from a 2D Human Pose Sequence. | Naoki Nishida, Yasutomo Kawanishi, Daisuke Deguchi, Ichiro Ide, Hiroshi Murase, Jun Piao |
| 2019 | RC | Characterizing Compatible View Updates in Syntactic Bidirectionalization. | Naoki Nishida, Germn Vidal |
| 2018 | FLOPS | CauDEr: A Causal-Consistent Reversible Debugger for Erlang. | Ivan Lanese, Naoki Nishida, Adrin Palacios, Germn Vidal |
| 2016 | LOPSTR | A Reversible Semantics for Erlang. | Naoki Nishida, Adrin Palacios, Germn Vidal |
| 2016 | PPDP | Proving inductive validity of constrained inequalities. | Takahiro Nagao, Naoki Nishida |
| 2015 | CADE | Confluence Competition 2015. | Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, Harald Zankl |
| 2015 | CADE | Reducing Relative Termination to Dependency Pair Problems. | Jos Iborra, Naoki Nishida, Germn Vidal, Akihisa Yamada |
| 2015 | LPAR | Constrained Term Rewriting tooL. | Cynthia Kop, Naoki Nishida |
| 2014 | APLAS | Automatic Constrained Rewriting Induction towards Verifying Procedural Programs. | Cynthia Kop, Naoki Nishida |
| 2013 | LOPSTR | A Finite Representation of the Narrowing Space. | Naoki Nishida, Germn Vidal |
| 2012 | LOPSTR | Computing More Specific Versions of Conditional Rewriting Systems. | Naoki Nishida, Germn Vidal |
| 2012 | LOPSTR | Improving Determinization of Grammar Programs for Program Inversion. | Minami Niwa, Naoki Nishida, Masahiko Sakai |
| 2010 | FLOPS | Proving Injectivity of Functions via Program Inversion in Term Rewriting. | Naoki Nishida, Masahiko Sakai |
| 2009 | LOPSTR | Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing. | Jos Iborra, Naoki Nishida, Germn Vidal |