小嶋 美咲（KOJIMA Misaki）

Misaki Kojima（小嶋 美咲）

名古屋大学 大学院情報学研究科 附属価値創造教育研究センター 特任助教

Designated Assistant Professor, Education and Research Center for Future Value Creation, Graduate School of Informatics, Nagoya University

博士（情報学）

Doctor of Informatics

所在地

Postal Address

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

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

居室

Office

IB電子情報館南棟5階 595

Room 595, IB south building

Eメールアドレス

E-mail

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

k-misaki [at] nagoya-u.jp

kojima.misaki.p4 [at] f.mail.nagoya-u.ac.jp

ホームページ（個人）

Homepage (Personal)

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

学位論文

Theses

1. Misaki Kojima,
   Runtime-Error Verification by Reduction to All-Path Reachability Problems of Constrained Rewriting,
   博士論文，名古屋大学 大学院情報学研究科，2024年1月．
2. Misaki Kojima,
   Runtime-Error Verification by Reduction to All-Path Reachability Problems of Constrained Rewriting,
   PhD thesis, Graduate School of Informatics, Nagoya University, January 2024.

発表論文

Selected Publications

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]


2. Misaki Kojima,
   On Transforming Prioritized Multithreaded Programs into Logically Constrained Term Rewrite Systems,
   the 62nd TRS meeting, Aichi, September 2025.


3. 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.


4. 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.


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, 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.


7. 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.


8. 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.


9. 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.


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. 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.


12. 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.


13. 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).


14. 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.


15. Misaki Kojima,
    From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting,
    the 59th TRS meeting, Izumo, September 2023.


16. 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.


17. 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.


18. 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.


19. 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.


20. 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.


21. 松見 歩佳，西田 直樹，小嶋 美咲，申東訓．
    ビットベクトル制約付き項書換え系の停止性証明のための多項式解釈プロセッサについて．
    電子情報通信学会技術報告 SS2022-61，Vol.122，No.432，pp.85-90，2023年3月．
22. 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).


23. 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, January 2023.


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


25. 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.


26. 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.


27. Misaki Kojima, Naoki Nishida, and Yutaka Matsubara.
    Transforming Concurrent Programs with Semaphores into Logically Constrained Term Rewrite Systems.
    Informal Proceedings of the 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2020), 12 pages, June 2020.


28. 小嶋 美咲，西田 直樹，酒井 正彦．
    計数セマフォを含むプログラムから論理制約付き項書換え系への変換．
    情報処理学会第83回全国大会論文集，No.6J07，pp.229-230，2021年3月．
29. Misaki Kojima, Naoki Nishida, and Masahiko Sakai.
    Transforming Programs with Counting Semaphores into Logically Constrained Term Rewrite Systems.
    Record of the 83rd National Convention of IPSJ, No.6J07, pp.229-230, March 2021.


30. 小嶋 美咲，西田 直樹，松原 豊，酒井 正彦．
    排他制御を含むプログラムから論理制約付き項書換え系への変換．
    電子情報通信学会技術報告 SS2019-46，Vol.119，No.451，pp.31-36，2020年3月．
31. Misaki Kojima, Naoki Nishida, Yutaka Matsubara, and Masahiko Sakai.
    Transforming Programs with Exclusive Control into Logically Constrained Term Rewrite Systems.
    IEICE Technical Report SS2019-46, Vol.119, No.451, pp.31-36, March 2020 (in Japanese).

出版物

Publications

1. 小嶋 美咲， Runtime-Error Verification via All-Path Reachability Problems of Constrained Rewriting， 情報処理学会「2023年度研究会推薦博士論文速報」，65巻11号，2024年
2. Misaki Kojima, Runtime-Error Verification via All-Path Reachability Problems of Constrained Rewriting, IPSJ FY2023 Doctoral Dissertations Recommended by Special Interest Groups, Vol. 61, No. 11, 2024.

受賞

Awards

1. 小嶋 美咲，情報処理学会山下記念研究賞，2025年3月14日．
2. Misaki Kojima, IPSJ Yamashita SIG Research Award, March 14, 2025.
3. 小嶋 美咲，情報処理学会東海支部学生論文奨励賞，2024年5月16日．
4. Misaki Kojima, IPSJ Tokai Branch Student Paper Encouragement Award, May 16, 2024.
5. 小嶋 美咲，情報処理学会第83回全国大会大会優秀賞，2021年6月2日．
6. Misaki Kojima, Best Paper Award of the 83th IPSJ National Convention, June 2, 2021.
7. 小嶋 美咲，情報処理学会第83回全国大会学生奨励賞，2021年3月20日．
8. Misaki Kojima, Student Encouragement Award of the 83th IPSJ National Convention, March 20, 2021.

略歴

Biography

学歴

Educational Background

職歴

Academic Career

学会活動

Society Activities

所属学会

Affiliated Academic Societies

• 情報処理学会
• Information Processing Society of Japan