西田 直樹（NISHIDA Naoki）

Naoki Nishida（西田 直樹）

名古屋大学 大学院情報学研究科 情報システム学専攻 計算論講座 教授

Professor, Department of Computing and Software Systems, Graduate School of Informatics, Nagoya University

博士（工学）

Doctor of Engineering

所在地

Postal Address

〒464-8601 名古屋市千種区不老町

Furo-cho, Chikusa-ku, Nagoya 4648601, Japan

居室

Office

IB電子情報館南棟5階 589

Room 589, IB south building

Tel

052-789-5141 業務に関係しない電話，お断り！！

+81-52-789-5141

Eメールアドレス

E-mail

nishida [at] i.nagoya-u.ac.jp

naoki.nishida [at] nagoya-u.jp

nishida.naoki.g5 [at] f.mail.nagoya-u.ac.jp

• 上記1つ目，2つ目のメールアドレスは上記3つ目のアドレスに転送されています．
• The first and second email addresses above have been forwarded to the third address above.
• 2024年4月以降，私に送信されたメール，私が送信したメールが届かない事例が発生しています．
• Since April 2024, there have been cases where emails sent to/by me have not been delivered.
• 返信がない場合などはお手数ですが，上記の3つ目のアドレスに直接，メールをお送りください．
• If you do not receive a reply, please send an email directly to the third address above.

ホームページ（個人）

Homepage (Personal)

http://www.trs.css.i.nagoya-u.ac.jp/~nishida/

研究者総覧

Nagoya University Profiles of Researchers

https://profs.provost.nagoya-u.ac.jp/html/100002731_ja.html

https://profs.provost.nagoya-u.ac.jp/html/100002731_en.html

ニュース

News

2024/09/01

2022年の発表実績を追加

September 1st, 2024

Added publications in 2022.

2023/10/08

本ページをリニューアル

October 8th, 2023

Renewed this page.

研究内容

Research Topics

• プログラム逆化
• Program inversion
• プログラム変換
• Program transformation
• 項書換え
• Term rewriting
• 制約付き書換え
• Constrained rewriting
• 条件付き書換え
• Conditional rewriting
• ナローイング
• Narrowing
• プログラム検証
• Program verification

発表論文

Publications

• 研究者総覧（名古屋大学）
• Researchers (Nagoya Univ.)
• DBLP (Naoki Nishida 0001)

学位論文

Theses

1. Naoki Nishida,
   Transformational Approach to Inverse Computation in Term Rewriting,
   博士論文，名古屋大学・大学院工学研究科，2004年1月．
2. Naoki Nishida,
   Transformational Approach to Inverse Computation in Term Rewriting,
   PhD thesis, Graduate School of Engineering, Nagoya University, January 2024.

ジャーナル（2022年度〜）

Journals (2022 - )

1. Naoki Nishida, Misaki Kojima, and Takumi Kato,
   Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms,
   Journal of Logical and Algebraic Methods in Programming, Vol. 145, 18 pages, May 2025.


2. Naoki Nishida, Misaki Kojima, and Ayuka Matsumi,
   A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems,
   Journal of Logical and Algebraic Methods in Programming, Vol. 144, 15 pages, March 2025.


3. Misaki Kojima, Naoki Nishida, and Yutaka Matsubara,
   Transforming concurrent programs with semaphores into logically constrained term rewrite systems,
   Journal of Logical and Algebraic Methods in Programming, Vol. 143, 23 pages, February 2025.


4. Misaki Kojima and Naoki Nishida,
   A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations,
   Journal of Information Processing, Vol. 32, pp. 417-435, May 2024.
   • Lemma 5.1 implicitly assumes that constrained terms ⟨s | φ⟩, ⟨t | ψ⟩ are linear. Generalization to arbitrary constrained terms is straightforward: as a preprocess, for each constrained term, we first linearize logical variables and append equality constraints to the constrained part.
   • Constraints φ and ψ are equivalent if Var(φ)=Var(ψ) and φ ↔ ψ is valid (w.r.t. the considered structure).


5. Misaki Kojima and Naoki Nishida,
   Reducing Non-Occurrence of Specified Runtime Errors to All-Path Reachability Problems of Constrained Rewriting,
   Journal of Logical and Algebraic Methods in Programming, Vol. 135, 19 pages, October 2023.


6. Shujun Zhang and Naoki Nishida,
   Transforming orthogonal inductive definition sets into confluent term rewrite systems,
   Journal of Logical and Algebraic Methods in Programming, Vol. 127, pp. 1-17, May 2022.

国際会議・ワークショップ（2022年度〜）

International Conferences and Workshops (2022 -)

1. Naoki Nishida, Misaki Kojima, and Yuto Nakamura,
   Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems,
   Proceedings of the 15th International Symposium on Frontiers of Combining Systems (FroCoS 2025), Lectures Notes in Computer Science, Vol. 15979, pp. 247–266, Springer, Cham, Reykjavik, Iceland, September 2025.
   [full version with complete proofs] [Recording]


2. Kanta Takahata, Jonas Schöpf, Naoki Nishida, and Takahito Aoto,
   Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations,
   Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming (PPDP 2025), Articile No. 9, pp. 1-13, ACM, Rende, Italy, September 2025.
   [full version with complete proofs]


3. Kanta Takahata, Jonas Schöpf, Naoki Nishida, and Takahito Aoto,
   Characterizing Equivalence of Logically Constrained Terms via Existentially Constrained Terms,
   Proceedings of the 35th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2025), Lectures Notes in Computer Science, Vol. 16117, pp. 180–195, Springer, Cham, Rende, Italy, September 2025.
   [full version with complete proofs]


4. Naoki Nishida and Raúl Gutiérrez:,
   Proceedings of the 14th International Workshop on Confluence,
   IWC 2025, Leipzig, Germany, September 2025.


5. Misaki Kojima and Naoki Nishida,
   On Transforming Prioritized Multithreaded Programs into Logically Constrained Term Rewrite Systems,
   Informal Proceedings of the 11th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2025), pp. 39-51,, Birmingham, UK, July 2025.


6. Naoki Nishida and Nozomi Taira,
   On Merging Constrained Rewrite Rules of Induction Hypotheses in Constrained Rewriting Induction,
   Informal Proceedings of the 11th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2025), pp. 85-96, Birmingham, UK, July 2025.


7. Misaki Kojima and Naoki Nishida,
   On Solving All-Path Reachability Problems for Starvation Freedom of Concurrent Rewrite Systems Under Process Fairness,
   Proceedings of the 18th International Conference on Reachability Problems (RP 2024),
   Lecture Notes in Computer Science, Vol. 15050, pp. 54-70, Springer Cham, September 2024.


8. Takahito Aoto, Naoki Nishida, and Jonas Schöpf,
   Equational Theories and Validity for Logically Constrained Term Rewriting,
   Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024),
   LIPIcs, Vol. 299, pp. 31:1-31:21, Tallinn, Estonia, July 2024.


9. Cyrille Chenavier and Naoki Nishida,
   Proceedings of the 13th International Workshop on Confluence,
   IWC 2024, Tallinn, Estonia, July 2024.


10. Misaki Kojima and Naoki Nishida,
    On Proving Confluence of Concurrent Programs by All-Path Reachability of LCTRSs,
    Proceedings of the 13th International Workshop on Confluence (IWC 2024), pp. 2-8, Tallinn, Estonia, July 2024.


11. Ayuka Matsumi, Naoki Nishida, Misaki Kojima, and Donghoon Shin,
    On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic,
    Proceedings of the 19th International Workshop on Termination (WST 2023), 6 pages, Obergurgl, Austria, August 2023.


12. Takahito Aoto, Nao Hirokawa, Dohan Kim, Misaki Kojima, Aart Middeldorp, Fabian Mitterwallner, Naoki Nishida, Teppei Saito, Jonas Schöpf, Kiraku Shintani, René Thiemann and Akihisa Yamada,
    A New Format for Rewrite Systems,
    Proceedings of the 12th International Workshop on Confluence (IWC 2023), pp. 32-37, Obergurgl, Austria, August 2023.


13. Naoki Nishida, Misaki Kojima, and Ayuka Matsumi,
    A Nesting-Preserving Transformation of SIMP Programs into Logically Constrained Term Rewrite Systems,
    Informal Proceedings of the 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2023), 11 pages, Rome, Italy, July 2023.


14. Misaki Kojima and Naoki Nishida,
    On Representations of Waiting Queues for Semaphores in Logically Constrained Term Rewrite Systems,
    Informal Proceedings of the 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2023), 6 pages, Rome, Italy, July 2023.


15. Misaki Kojima and Naoki Nishida,
    From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting,
    Proceedings of the 25th International Symposium on Practical Aspects of Declarative Languages (PADL 2023),
    Lecture Notes in Computer Science, Vol. 13880, pp. 161-179, Springer, Cham, Boston, USA, January 2023.


16. Naoki Nishida and Misaki Kojima,
    CO3 (Version 2.3),
    Proceedings of the 11th International Workshop on Confluence (IWC 2022), page 63, August 2022.


17. Raúl Gutiérrez, Aart Middeldorp, Naoki Nishida, and Kiraku Shintani,
    Confluence Competition 2022,
    Proceedings of the 11th International Workshop on Confluence (IWC 2022), page 54, August 2022.


18. Shujun Zhang and Naoki Nishida,
    On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs,
    Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022), 14 pages, July 2022.


19. Misaki Kojima and Naoki Nishida,
    On Reducing Non-Occurrence of Specified Runtime Errors to All-Path Reachability Problems of Constrained Rewriting,
    Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022), 16 pages, July 2022.


20. Naoki Nishida, Misaki Kojima, and Takumi Kato,
    On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms,
    Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022), 16 pages, July 2022.


21. Shujun Zhang and Naoki Nishida,
    On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs,
    Proceedings of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022), Lecture Notes in Computer Science, Vol. 13215, pp. 262-281, Springer, May 2022.

国内会議・研究会（2022年度〜）

Domestic Events (2022 -)

1. 高畑 幹汰，Jonas Schöpf，西田 直樹，青戸 等人，
   論理制約付き項書き換えシステムにおける制約付き最汎書き換え，
   第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）， 2025年3月．
2. Kanta Takahata, Jonas Schöpf, Naoki Nishida, and Takahito Aoto,
   Most General Constrained Rewriting of Logically Constrained Term Rewriting Systems,
   the 27th Workshop on Programming and Programming Languages (PPL 2025), March 2025.


3. 平等 望，西田 直樹，酒井 正彦，
   制約付き書換え帰納法による証明における選言型制約を持つ等式の分割の完全性について，
   令和6年度電気・電子・情報関係学会東海支部連合大会講演論文集， No. H6-4，1ページ，2024年8月．
4. Nozomi Taira, Naoki Nishida, and Masahiko Sakai,
   On completeness of decomposion of equations with disjunctive constraints on provability of constrained rewriting induction,
   Record of 2024 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering, No. H6-4, 1 page, August 2024.


5. Misaki Kojima and Naoki Nishida,
   A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-Path Reachability Problems with Constant Destinations,
   情報処理学会・第146回プログラミング研究発表会， 発表資料 2023-3-(1)，17ページ，2023年10月．
6. Misaki Kojima and Naoki Nishida,
   A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-Path Reachability Problems with Constant Destinations,
   Presentation at the 146th Meeting on IPSJ Special Interest Group on Programming, No. 2023-3-(1), 17 pages, October 2023.


7. 松見 歩佳，西田 直樹，小嶋 美咲，申東訓，
   ビットベクトル制約付き項書換え系の停止性証明のための多項式解釈プロセッサについて，
   電子情報通信学会技術報告 SS2022-61，Vol.122，No.432，pp.85-90，2023年3月．
8. Ayuka Matsumi, Naoki Nishida, Misaki Kojima, and Donghoon Shin,
   On Polynomial Interpretations Toward Termination of Logically Constrained Term Rewrite Systems with Bit Vector Arithmetic,
   IEICE Technical Report SS2022-61, Vol.122, No.432, pp.85-90, March 2023 (in Japanese).


9. 熊谷 妃美香，西田 直樹，
   プログラム逆化のための文脈自由表現の等価関係に基づく項書換え系決定化手法の実装，
   情報処理学会第83回全国大会講演論文集， No. 1L-05, pp. 271-272, 2022年3月．
10. Himika Kumagai and Naoki Nishida,
    Implementing Determinization of Term Rewrite Systems via Equivalence of Context-Free Expressions toward Program Inversion,
    Record of the 84th National Convention of IPSJ, No. 1L-05, pp. 271-272, March 2022 (in Japanese).


11. 加藤 拓洋，西田 直樹，酒井 正彦，
    LLVM中間表現の意味論規則を表現する制約付き書換え規則について，
    信学技法 SS2021-34， Vol. 121, No. 318, pp. 89-94，電子情報通信学会，2022年1月．
12. Takumi Kato, Naoki Nishida, and Masahiko Sakai,
    On Constrained Rewrite Rules Representing Semantics Rules of LLVM IR,
    IEICE Technical Report SS2021-34, Vol. 121, No. 318, pp. 89-94, the Institute of Electronics, Information and Communication Engineers (IEICE), January 2022 in Japanese).

招待講演

Invited Talks

1. Naoki Nishida,
   Unravelings and Narrowing Trees Towards Confluence of Deterministic CTRSs,
   the 12th International Workshop on Confluence (IWC 2023), Obergurgl, Austria, August 2023.

口頭発表（2022年度〜）

Oral Presentations (2022 -)

1. Naoki Nishida,
   Difference of Constrained Terms in LCTRSs,
   the 62nd TRS meeting, Aichi, September 2025.


2. Naoki Nishida and Misaki Kojima,
   CO3 (Version 2.6),
   Proceedings of the 14th International Workshop on Confluence (IWC 2025), pp. 65-66, Leipzig, Germany, September 2025.


3. Naoki Nishida and Misaki Kojima,
   CRaris (Version 1.1),
   Proceedings of the 14th International Workshop on Confluence (IWC 2025), pp. 67-68, Leipzig, Germany, Septebmer 2025.


4. Raúl Gutiérrez, Aart Middeldorp, Naoki Nishida, Teppei Saito, and Reé Thiemann,
   Confluence Competition 2025,
   Proceedings of the 14th International Workshop on Confluence (IWC 2025), pp. 52-53, September 2025.


5. Naoki Nishida,
   A Proof System for All-Path Reachability Problems of LCTRSs,
   a seminar at Radboud University Nijmegen, June 2025.


6. Naoki Nishida,
   All-Path Reachability for Starvation Freedom Under Process Fairness,
   the 60th TRS meeting, Tokyo, October 2024.


7. Raúl Gutiérrez, Aart Middeldorp, Naoki Nishida, Teppei Saito, and Reé Thiemann,
   Confluence Competition 2024,
   Proceedings of the 13th International Workshop on Confluence (IWC 2024), pp. 63-64, July 2024.


8. Naoki Nishida and Misaki Kojima,
   CO3 (Version 2.5),
   Proceedings of the 13th International Workshop on Confluence (IWC 2024), pp. 71-72, Tallinn, Estonia, July 2024.


9. Naoki Nishida and Misaki Kojima,
   CRaris: CR checker for LCTRSs in ARI Style,
   Proceedings of the 13th International Workshop on Confluence (IWC 2024), pp. 83-84, Tallinn, Estonia, July 2024.


10. Naoki Nishida,
    On Constrained Narrowing of Logically Constrained Term Rewrite Systems,
    the 59th TRS meeting, Izumo, September 2023.


11. Raúl Gutiérrez, Aart Middeldorp, Naoki Nishida, and Kiraku Shintani,
    Confluence Competition 2023,
    Proceedings of the 12th International Workshop on Confluence (IWC 2023), pp. 61-62, August 2023.


12. Naoki Nishida, Misaki Kojima, Ayuka Matsumi,
    CO3 (Ver. 2.4),
    Proceedings of the 12th International Workshop on Confluence (IWC 2023), p. 67, Obergurgl, Austria, August 2023.


13. Naoki Nishida,
    On Transforming Imperative Programs into LCTRSs via Injective Functions from Configurations to Terms,
    Presentation at the 57th TRS Meeting, September 2022.


14. Naoki Nishida and Misaki Kojima,
    CO3 (Version 2.3),
    Proceedings of the 11th International Workshop on Confluence, p. 63, August 2022.


15. Naoki Nishida,
    Inversion and Determinization in Term Rewriting,
    Presentation at the meeting of IFIP Working Group 1.6: Rewriting, July 2022.


16. Naoki Nishida,
    On Semantically Equivalent Operations for Inversion of DCTRSs,
    Presentation at the 56th TRS Meeting, February 2022.

受賞

Awards

• 情報処理学会論文編集貢献賞（2020/05/12）
• 情報処理学会研究活動貢献励賞（2020/02/18）
• 平成24年度電子情報通信学会ソフトウェアサイエンス研究会 研究奨励賞（2013/05/09）

  講演題目・著者・発表研究会

  Malbolge低級アセンブリプログラミングにおける制御命令の配置設計のためのSATソルバの利用，安藤聡，酒井正彦，坂部俊樹，草刈圭一朗，西田直樹，平成25年1月電子情報通信学会ソフトウェアサイエンス研究会

• 平成23年度電子情報通信学会ソフトウェアサイエンス研究会 研究奨励賞（2012/05/10）

  講演題目・著者・発表研究会

  2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み，日野善信，酒井正彦，坂部俊樹，草刈圭一朗，西田直樹，平成23年10月電子情報通信学会ソフトウェアサイエンス研究会

  講演題目・著者・発表研究会

  語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて，坂井利光，酒井正彦，坂部俊樹，西田直樹，草刈圭一朗，平成24年1月電子情報通信学会ソフトウェアサイエンス研究会

• 第67回（平成22年度）電子情報通信学会論文賞（2011/05/28）
• 67th Best Paper Award of IEICE (May 28th, 2011)
• 平成14年度電気関係学会東海支部連合大会 奨励賞（2003/01/27）

開発ツール

Tools

• Repius
• CO3
• Crisys
• CRaris

略歴

Biography

学歴

Educational Background

職歴

Academic Career

学会活動

Society Activities

所属学会

Affiliated Academic Societies

• 日本ソフトウェア科学会（JSSST）
• Japan Sociery of Software Science and Technologies (JSSST)
• 電子情報通信学会（IEICE）
• The Institute of Electronics, Information and Communication Engineers (IEICE)
• 情報処理学会（IPSJ）
• Information Processing Society of Japan (IPSJ)

編集委員

Editorial Committee Members

• 情報処理学会・論文誌プログラミング・編集委員長（2018年4月〜2020年3月）
• IPSJ Transaction on Programming, editor-in-chief (April 2018 - March 2020)
• 情報処理学会・論文誌プログラミング（2013年4月〜2017年3月，2020年4月〜2024年3月）
• IPSJ Transaction on Programming (April 2013 - March 2017, April 2020 - March 2024)

プログラム委員

Program Committee Members

• IWC 2025 (PC co-chair)
• FSCD 2025
• PADL 2025
• 第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）
• PPL 2025
• IWC 2024 (PC co-chair)
• FSCD 2024
• CADE 2023
• 第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2022）
• PPL 2022
• LOPSTR 2022
• IWC 2022
• LOPSTR 2021
• FSCD 2021
• PPDP 2017
• WPTE 2017
• SCSS 2017
• LOPSTR 2016
• WPTE 2016
• WPTE 2015 (PC co-chair)
• LOPSTR 2014
• 第12回プログラミングおよびプログラミング言語ワークショップ（PPL 2010）
• PPL 2010
• PEPM 2009

舵取り委員

Steering Committee Members

• IWC (September 2025 -)
• Confluence Competition (CoCo) (September 2019 -)
• WPTE (2015 -)

その他

Other Committee Members

• 2023年度電子情報通信学会ソサイエティ大会 現地開催校委員
• IFIP WG 1.6: Rewriting, member (August 2022 - present)
• 情報処理学会プログラミング研究会・幹事（2020年4月〜2024年3月）
• 情報処理学会・代表員（2019年4月〜2021年3月）
• 2019年度LAシンポジウム事務局メンバー（2019年4月〜2020年3月）
• 第81回情報処理学会全国大会実行委員会・プログラム編成WG委員
• CoCo 2018, organization committee member
• 電子情報通信学会ソフトウェアサイエンス研究専門委員会・専門委員（2018年6月〜2024年6月）
• 情報処理学会プログラミング研究会・コンピュータサイエンス領域委員会・委員（2018年4月〜2020年3月）
• 情報処理学会プログラミング研究会・主査（2018年4月〜2020年3月）
• IPSJ Special Interest Group on Programming, chief examiner (April 2018 - March 2020)
• CoCo 2017, organization committee member
• WPTE 2017, organization committee member
• 第79回情報処理学会全国大会実行委員会・実行委員
• CoCo 2016, organization committee member
• WPTE 2016, organization committee member
• 情報処理学会プログラミング研究会・運営委員（2014年4月〜2018年3月）
• 情報処理学会・代表員（2013年4月〜2014年3月）
• 平成24年度電気関係学会東海支部大会・実行委員
• 情報処理学会東海支部・幹事（2012年4月〜2014年5月）
• 2011年度LAシンポジウム事務局メンバー（2011年4月〜2012年3月）
• RTA 2012, local organization member
• IWC 2012, local representative
• 名報会・役員（2008年5月〜現在）

リンク

Links

• 酒井・西田研究室
• Sakai-Nishida Laboratory
• 情報学部・情報学研究科
• School & Graduate School of Informatics
• 名古屋大学
• Nagoya University
• 東海国立大学機構
• Tokai National Higher Education and Research System