Yusuke MATSUSHITA (松下 祐介)

(Last updated: Mar 7, 2026)

I am a software scientist working as a Program-Specific Assistant Professor at the Hakubi Center for Advanced Research and the Graduate School of Informatics, Kyoto University.
I specialize in formal verification of stateful programs, especially those written in Rust (e.g., RustHorn, RustHornBelt, Nola, Pure Borrow, and VerusBelt). I am also curious about many other topics, including quantum computing (e.g., RapunSL) and algorithms (e.g., SoftMatcha, SoftMatcha 2).

Self-introduction at the Hakubi Center.

Google Scholar, ORCID, researchmap, dblp
GitHub, Twitter, LinkedIn
Email: ysk.m24t@gmail.com

Curriculum Vitae (Last updated: Mar 7, 2026)

Work

• Apr 2026 – (Mar 2028).
  Visiting Scientist at MPI-SWS, Germany. Host: Derek Dreyer.
• Apr 2025 – (Mar 2030).
  Program-Specific Assistant Professor at the Hakubi Center for Advanced Research, Kyoto University.
  For the project “Exploring a New Age of Software Development Springing from Rust”.
  Awarded the title of Hakubi Researcher on Apr 1, 2025.
  Host: Atsushi Igarashi, the Computer Software Group, Grad School of Informatics, Kyoto University.
  Self-introduction as a Hakubi researcher: Web page.
  Info about the selection: Web page.
• Apr 2024 – Mar 2025.
  JSPS Fellow (PD) at the Computer Software Group, Grad School of Informatics, Kyoto University.

Education

• Apr 2021 – Mar 2024.
  Doctor of Philosophy in the field of Information Science and Technology.
  Dept. of Computer Science, Grad School of IST, University of Tokyo. Supervisor: Naoki Kobayashi.
• Apr 2019 – Mar 2021.
  Master of Information Science and Technology.
  Dept. of Computer Science, Grad School of IST, University of Tokyo. Supervisor: Naoki Kobayashi.
• Apr 2017 – Mar 2019.
  Bachelor of Science.
  Dept. of Information Science, School of Science, University of Tokyo. Supervisor: Naoki Kobayashi.
• Apr 2015 – Mar 2017.
  Natural Sciences I, College of Arts and Sciences Junior Div., UTokyo.
• Apr 2009 – Mar 2015.
  Nada Junior and Senior High School.

Papers

• Masataka Yoneda, Yusuke Matsushita, Go Kamoda, Kohei Suenaga, Takuya Akiba, Masaki Waga and Sho Yokoi.
  SoftMatcha 2: A Fast and Soft Pattern Matcher for Trillion-Scale Corpora..
  arXiv. Feb 11, 2026.
  Website, Demo, Code.
  Paper: arXiv.
• Travis Hance, Laila Elbeheiry, Yusuke Matsushita, Derek Dreyer.
  VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System.
  Conditionally accepted for PLDI 2026. June 15-19, 2026.
• Yusuke Matsushita and Hiromi Ishii.
  Pure Borrow: Linear Haskell Meets Rust-Style Borrowing.
  Conditionally accepted for PLDI 2026. June 15-19, 2026.
• Yusuke Matsushita*, Kengo Hirata*, Ryo Wakizaka and Emanuele D’Osualdo (*: equal contribution).
  RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing.
  POPL 2026. Jan 11-17, 2026.
  Paper: ACM-DL, arXiv, Authors’.
• Yusuke Matsushita and Takeshi Tsukada.
  Nola: Later-Free Ghost State for Verifying Termination in Iris.
  PLDI 2025. June 16-20, 2025.
  Paper: ACM-DL, Authors’.
  Rocq artifact: GitHub, Zenodo.
  Talk at PLDI 2025: Slides, YouTube.
  Talk at Iris Workshop 2025: Slides.
• Hiroyuki Deguchi, Go Kamoda, Yusuke Matsushita, Chihiro Taguchi, Kohei Suenaga, Masaki Waga and Sho Yokoi.
  SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches.
  ICLR 2025. Apr 24-28, 2025.
  Website, Demo, Code, OpenReview.
  Paper: OpenReview, arXiv.
• Takashi Nakayama, Yusuke Matsushita, Ken Sakayori, Ryosuke Sato and Naoki Kobayashi.
  Borrowable Fractional Ownership Types for Verification.
  VMCAI 2024. Jan 15-16, 2024.
  Paper: Springer, arXiv.
  Talk at VMCAI 2024: YouTube.
• Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan and Derek Dreyer.
  RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code.
  PLDI 2022. June 13-17, 2022.
  Distinguished Paper Award.
  Paper: ACM-DL, Authors’.
  Artifacts: Zenodo; Rocq mechanization, Benchmarks.
  Talk at PLDI 2022: Slides, YouTube.
• Yusuke Matsushita, Takeshi Tsukada and Naoki Kobayashi.
  RustHorn: CHC-based Verification for Rust Programs.
  TOPLAS. Oct 31, 2021.
  Extended version of the same-titled ESOP 2020 paper.
  Paper: ACM-DL, Authors’.
• Yusuke Matsushita, Takeshi Tsukada and Naoki Kobayashi.
  RustHorn: CHC-based Verification for Rust Programs.
  ESOP 2020. Apr 27-29, 2020.
  Selected to TOPLAS Special Issue on ESOP 2020.
  Paper: Authors’, Springer, arXiv.
  Talk at ESOP 2020: Slides (Keynote), Video.
  Artifacts: Zenodo, GitHub Repo.

Theses

• Yusuke Matsushita.
  Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows (不変条件と Rust 流の借用を扱える非 Step-Indexed な分離論理).
  Ph.D. dissertation. University of Tokyo. Supervised by Prof. Naoki Kobayashi. Dec 6, 2023.
  Precursor to the Nola paper.
  Paper: Author’s.
  Talk: Slides (Keynote).
• Yusuke Matsushita.
  Extensible Functional-Correctness Verification of Rust Programs by the Technique of Prophecy (預言の技術による Rust プログラムの拡張可能な機能正当性検証).
  Master’s thesis. University of Tokyo. Supervised by Prof. Naoki Kobayashi. Feb 24, 2021.
  Precursor to the RustHornBelt paper.
  Paper: Author’s.
  Talk: Slides (Keynote).
• Yusuke Matsushita.
  CHC-based Program Verification Exploiting Ownership Types (所有権型を利用した CHC ベースのプログラム検証).
  Senior thesis. University of Tokyo. Supervised by Prof. Naoki Kobayashi. Feb 28, 2019.
  Precursor to the RustHorn paper.
  Paper: Author’s.
  Talk: Slides (Keynote).

Lectures

• Yusuke Matsushita. Science of Software, the Fun of Rust.
  Hakubi Seminar No. 273. Sept 2, 2025. Slides (Keynote). Info.
• Yusuke Matsushita. The Fun of Rust.
  Lecture for the Course of CCE, Grad School of Informatics, Kyoto University. Dec 20, 2024.
  Slides (Keynote), Info.
• Yusuke Matsushita. 分離論理 Iris の世界 (The World of the Separation Logic Iris).
  Invited lecture at PPL Summer School 2024. Sept 9, 2024.
  Slides (Keynote), YouTube.
• Yusuke Matsushita and Takashi Nakayama. ソフトウェアの科学 〜バグのない世界を目指して〜 (Science of Software, Aspiring to a World Free of Bugs).
  Open Campus 2023, the Faculty of Science, the University of Tokyo. Aug 2, 2023.
  Slides (Keynote), YouTube.

Articles

• Yusuke Matsushita. Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows.
  2023 年度研究会推薦博士論文速報 (Bulletin of Ph.D. Dissertations in AY 2023 Recommended by SIGs), Information Processing Society of Japan. Aug 15, 2024.
  HTML (Japanese)
• Yusuke Matsushita. ソフトウェアの世界を切り拓く (Breaking Ground in the World of Software).
  理学のススメ (An Encouragement of Science) No. 7 in the University of Tokyo 理学部ニュース (News from Faculty of Science) Vol. 54, No. 1, May 20, 2022.
  Text: Author’s (Japanese & English); PDF, HTML (Japanese).

Talks

• Yusuke Matsushita and Takeshi Tsukada.
  Nola: Later-Free Ghost State for Verifying Termination in Iris. PLDI 2025.
  Talk at PLDI 2025. June 21, 2025. Slides (Keynote), YouTube. Talk at Iris Workshop 2025. June 2, 2025. Slides (Keynote).
• Yusuke Matsushita, Kengo Hirata and Ryo Wakizaka.
  Concurrent Quantum Separation Logic for Fine-Grained Parallelism.
  Talk at TPSA 2025. Jan 21, 2025. Extended abstract, Slides (Powerpoint).
  Talk at PLanQC 2025 (Presented by Ryo Wakizaka). Jan 25, 2025. Extended abstract, Slides (Powerpoint).
• Yusuke Matsushita.
  Rust から広がるプログラム検証・テストの新展望 (New Perspectives on Program Verification and Testing Spreading from Rust).
  Invited talk at PRO-2024-1. June 13, 2024. Slides (Keynote).
• Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan and Derek Dreyer.
  RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. PLDI 2022.
  Talk at PLDI 2022. June 17, 2022. Slides, YouTube.
• Yusuke Matsushita, Takeshi Tsukada and Naoki Kobayashi.
  RustHorn: CHC-based Verification for Rust Programs. ESOP 2020.
  Talk at ESOP 2020. Mar 31, 2021 (delayed due to the pandemic). Slides (Keynote), Video.
  Invited talk at JSSST 2020. Sept 10, 2020. Slides (Keynote), YouTube.
  Talk at PPL 2020. Mar 4, 2020. Slides (Keynote).

Co-Authored

• Masataka Yoneda, Go Kamoda, Yusuke Matsushita, Kohei Suenaga, Takuya Akiba, Masaki Waga and Sho Yokoi.
  SoftMatcha 2: 1兆語規模コーパスの超高速かつ柔らかい検索 (SoftMatcha 2: Ultra-Fast and Soft Searcher for Trillion-Scale Corpora).
  Precursor to SoftMatcha 2.
  NLP 2026. Mar 10, 2026.
  Paper.
• Hiroyuki Deguchi, Go Kamoda, Yusuke Matsushita, Chihiro Taguchi, Kohei Suenaga, Masaki Waga and Sho Yokoi.
  SoftMatcha: 大規模コーパス検索のための柔らかくも高速なパターンマッチャー (SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches).
  Precursor to SoftMatcha.
  NLP 2025. Mar 13, 2025.
  Paper.

Posters

• Yusuke Matsushita, Yudai Tanabe, Taro Sekiyama and Atsushi Igarashi.
  Linear Haskell での Rust 流借用の純粋な実現 (Pure Realization of Rust-Style Borrows in Linear Haskell).
  PPL 2025. Mar 5, 2025. PDF (Keynote).
  Best Poster Award.
• Yusuke Matsushita, Naoki Kobayashi and Takeshi Tsukada.
  所有権型を利用した CHC ベースのプログラム検証 (CHC-based Program Verification Exploiting Ownership Types).
  PPL 2019. Mar 6, 2019. PDF (Keynote).

Co-Authored

• Masayuki Goto, Yusuke Matsushita and Atsushi Igarashi.
  型に基づくRust API探索の手法と実装 (Methods and Implementation of Type-based Rust API Search).
  PPL 2026. Mar 10, 2026.
• Musashi Katsura, Yusuke Matsushita, Ken Sakayori and Naoki Kobayashi.
  動的な借用検査を活用したUnsafe Rustコードの正当性検査 (Testing Correctness of Unsafe Rust Code Using Dynamic Borrow Checking).
  PPL 2026. Mar 10, 2026.
• Hirotaka Okada, Yusuke Matsushita and Atsushi Igarashi.
  Rustライブラリのスレッド安全性に関するバグのプログラム合成による発見 (Finding Thread-Safety Bugs in Rust Libraries Using Program Synthesis).
  PPL 2026. Mar 10, 2026.
• Sota Sato, Yusuke Matsushita, Kohei Suenaga and Atsushi Igarashi.
  関数型言語のバグ発見のための篩型システム (A Refinement Type System for Finding Bugs in Functional Language).
  PPL 2026. Mar 10, 2026.
• Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga and Atsushi Igarashi.
  ポインタ演算と多次元配列のための所有権篩型システム (An Ownership Refinement Type System for Pointer Arithmetic and Nested Arrays).
  PPL 2026. Mar 10, 2026.
• Hiroyuki Deguchi, Go Kamoda, Yusuke Matsushita, Chihiro Taguchi, Kohei Suenaga, Masaki Waga and Sho Yokoi.
  SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches.
  ICLR 2025. Apr 24, 2025.
  ICLR page, Webpage, OpenReview.
• Takashi Nakayama, Yusuke Matsushita, Ken Sakayori and Naoki Kobayashi.
  メモリ安全性のためのC++オブジェクトモデルのハイレベルな形式化 (High-Level Formalization of the C++ Object Model for Memory Safety).
  PPL 2025. Mar 5, 2025.
  Best Student Poster Award.
• Sota Sato, Yusuke Matsushita, Kohei Suenaga and Atsushi Igarashi.
  関数型言語のためのHyper Hoare Typeにむけて (Towards Hyper Hoare Types for Functional Languages). PPL 2025. Mar 5, 2025.
• Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga and Atsushi Igarashi.
  多重配列を扱う命令型プログラムの所有権と篩型の組み合わせによる形式検証 (Formally Verifying Imperative Programs with Nested Arrays by Combining Ownership and Refinement Types).
  PPL 2025. Mar 7, 2025.
• Yusuke Fujiwara, Yusuke Matsushita, Kohei Suenaga and Atsushi Igarashi.
  Towards Ownership Refinement Type Inference with Nested Arrays.
  APLAS 2024 Student Research Competition and Posters (Non-SRC). Oct 22, 2024.
• Hiroyuki Deguchi, Go Kamoda, Yusuke Matsushita, Kai Keida, Masaki Waga and Sho Yokoi.
  柔らかいgrep/KWICに向けて：高速単語列マッチングの埋め込み表現による連続化 (Towards Soft Grep/KWIC: Making Fast Word Sequence Matching Continuous Using Embedded Representations).
  YANS 2024. Sept 5, 2024.
  Precursor to SoftMatcha.
  Best Demo Award and Award by Recruit Holdings.
• Takashi Nakayama, Naoki Kobayashi, Ryosuke Sato and Yusuke Matsushita.
  命令型プログラムの検証のためのライフタイム付き分数所有権型システム (Fractional Ownership Type System with Lifetimes for Verifying Imperative Programs)
  PPL 2023. Mar 7, 2023.

Grants & Fellowships

• Apr 2026 - (Mar 2028)
  JSPS (学振) Overseas Research Fellowship (海外特別研究員).
  Host: Derek Dreyer, MPI-SWS, Germany.
  Exploring New Foundations for Software Development in the Age of Rust (Rust 時代におけるソフトウェア開発の新しい基礎の探究).
• Apr 2025 – (Mar 2030)
  The Hakubi Project, Kyoto University.
  Exploring a New Age of Software Development Springing from Rust (Rust から広がる新時代のソフトウェア開発の探究).
• Apr 2024 – Mar 2027.
  JSPS (学振) Research Fellowship for Young Scientists PD
  Foundations and Applications for Robust and High-Performance System Software (堅牢で高性能なシステムソフトウェアのための基礎と応用).
  KAKEN Page.
• Apr 2021 – Mar 2024.
  JSPS (学振) Research Fellowship for Young Scientists DC1
  Theory and Application for Robust and High-Performance Systems Programming Languages (堅牢で高性能なシステムプログラミング言語のための理論と応用).
  KAKEN Page.

Service

• Jul 2026 – Nov 2026.
  Program Committee member of POPL 2027.
• Jan 2026 – Mar 2026.
  Program Committee member of PPL 2026.
• Nov 2025 – Apr 2026.
  Review Committee member of PLDI 2026.
• Feb 2025 – Mar 2025.
  External reviewer of PLDI 2025.
• Jan 2025 – Mar 2025.
  Program Committee member of PPL 2025.

Teaching

• Aug 2025.
  Lecturer of L1 Rust 検証器自作ゼミ (Rust Verifier Development Seminar) at Security Camp 2025 by IPA.
• Aug 2024.
  Lecturer of S15 Rust プログラム検証ゼミ (Rust Program Verification Seminar) at Security Camp 2024 by IPA.
  • Blog articles “Rust で預言を使ったプログラム検証器を自作しよう (Let’s develop a prophecy-based program verifier in Rust by yourself)” by isan, a student of the seminar: #1, #2, #3.
• Apr 2022 – Aug 2022, Apr 2019 – Aug 2019.
  Teaching assistant of “Functional and Logic Programming Experiments” at Dept. of Information Science, School of Science, UTokyo.
• Sept 2019 – Feb 2020.
  Teaching assistant of “Processor and Compiler Experiments” at Dept. of Information Science, School of Science, UTokyo.
• Mar 2018.
  Lecturer of “Purely Functional Data Structures” at JOI 2017 Spring Training Camp.
• Aug 2017.
  Tutor on “Purely Functional Data Structures” (Chris Okasaki) at JOI 2017 Summer Seminar.

Internship

• Nov 2022 – Feb 2023.
  Software engineer internship for Google ChromeOS, at Google Tokyo.
• Sept 2020 – June 2021.
  Visiting Scholar (Online) at the RustBelt Team, MPI-SWS, supervised by Derek Dreyer.
• Aug 2019 – Jan 2020.
  Frontend and backend web engineer at CADDi (building a manufacturing platform), Tokyo, Japan
  Interview Article.
• Mar 2017 – Mar 2019.
  Software engineer at Morishita Lab (studying genome informatics), Dept. of Computational Biology and Medical Sciences, Grad School of Frontier Sciences, UTokyo, Japan.

Experiences

Competitive Programming

• AtCoder.
• Contestant of the ACM International Collegiate Programming Contest (ICPC) Asia Regionals of 2019 (Yokohama), 2018 (Yokohama) and 2016 (Tsukuba).
• Finalist of the Japanese Olympiad in Informatics (JOI) 2013 and 2012.
• Tutor of Japan’s special team of the International Olympiad in Informatics (IOI) 2018.

Piano and Music

• YouTube Channel @y.matsushita
• Mar 2022.
  Gold Prize of Japan J.S. Bach Music Concours.
• Dec 2019.
  Finalist of Japan J.S. Bach Music Concours.
• Dec 2015 – Dec 2016.
  Leader of Piano Society, UTokyo.

Debate

• Dec 2013.
  Best 8 finalist of National High School English Debate Tournament as a team of Nada High School.