Basic Information

Email Address

• Email Address

  matsushita.yusuke.3xkyoto-u.ac.jp

Academic Degree

• 19 Mar. 2021

  東京大学修士（情報理工学）
• 21 Mar. 2024

  東京大学博士（情報理工学）

Academic Resume (Graduate Schools)

• 東京大学, 大学院情報理工学系研究科コンピュータ科学専攻修士課程, 修了
• 東京大学, 大学院情報理工学系研究科コンピュータ科学専攻博士課程, 修了

Academic Resume (Undergraduate School/Majors)

• 東京大学, 理学部情報科学科, 卒業
• 東京大学, 教養学部前期課程理科一類

Research History

• From Apr. 2025, To Mar. 2030

  Kyoto University, Hakubi Center for Advanced Research, Program-Specific Assistant Professor
• From Apr. 2024, To Mar. 2025

  Kyoto University, Graduate School of Informatics Department of Communications and Computer Engineering, Program-Specific Researcher (JSPS PD)

ID,URL

• ORCID ID

  0000-0002-5208-3106

• J-Global ID

  202501004448074810

• Researcher number

  41003875

• External link

  https://shiatsumat.github.io

researchmap URL

• https://researchmap.jp/y.matsushita

Research

Research Interests

• Formal Verification
• Software Science
• Rust

Research Areas

• Informatics, Software, Software Science

Papers

• Prophecy-Based Automated Verification of Message-Passing Programs

  Takashi Nagatomi; Musashi Katsura; Naoki Kobayashi; Yusuke Matsushita; Ken Sakayori

  37th International Conference on Concurrency Theory (CONCUR 2026), 24 Aug. 2026, Peer-reviewed

  
• Prophecy-Based Automated Verification of Message-Passing Programs

  Takashi Nagatomi; Musashi Katsura; Naoki Kobayashi; Yusuke Matsushita; Ken Sakayori

  arXiv, 26 Jun. 2026

  
• Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

  Yusuke Fujiwara; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi

  40th European Conference on Object-Oriented Programming (ECOOP 2026), 25 Jun. 2026, Peer-reviewed

  
• VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System

  Travis Hance; Laila Elbeheiry; Yusuke Matsushita; Derek Dreyer

  Proceedings of the ACM on Programming Languages, 08 Jun. 2026, Peer-reviewed

  
• Pure Borrow: Linear Haskell Meets Rust-Style Borrowing

  Yusuke Matsushita; Hiromi Ishii

  Proceedings of the ACM on Programming Languages, 08 Jun. 2026, Peer-reviewed, Lead author

  
• SoftMatcha 2: A Fast and Soft Pattern Matcher for Trillion-Scale Corpora

  Masataka Yoneda; Yusuke Matsushita; Go Kamoda; Kohei Suenaga; Takuya Akiba; Masaki Waga; Sho Yokoi

  Proceedings of the 43rd International Conference on Machine Learning (ICML '26), 06 Jul. 2026, Peer-reviewed

  
• Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

  Yusuke Fujiwara; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi

  arXiv, 24 Apr. 2026, Lead author

  
• Pure Borrow: Linear Haskell Meets Rust-Style Borrowing

  Yusuke Matsushita; Hiromi Ishii

  arXiv, 16 Apr. 2026, Lead author

  
• SoftMatcha 2: A Fast and Soft Pattern Matcher for Trillion-Scale Corpora

  Masataka Yoneda; Yusuke Matsushita; Go Kamoda; Kohei Suenaga; Takuya Akiba; Masaki Waga; Sho Yokoi

  arXiv, 11 Feb. 2026

  
• RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing

  Yusuke Matsushita; Kengo Hirata; Ryo Wakizaka; Emanuele D'Osualdo

  Proceedings of the ACM on Programming Languages, 08 Jan. 2026, Peer-reviewed, Lead author

  
• RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing

  Yusuke Matsushita; Kengo Hirata; Ryo Wakizaka; Emanuele D'Osualdo

  arXiv, 28 Nov. 2025, Lead author

  
• Nola: Later-Free Ghost State for Verifying Termination in Iris

  Yusuke Matsushita; Takeshi Tsukada

  Proceedings of the ACM on Programming Languages, 13 Jun. 2025, Peer-reviewed, Lead author

  
• SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches

  Hiroyuki Deguchi; Go Kamoda; Yusuke Matsushita; Chihiro Taguchi; Kohei Suenaga; Masaki Waga; Sho Yokoi

  13th International Conference on Learning Representations (ICLR 2025), Apr. 2025, Peer-reviewed

  
• SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches

  Hiroyuki Deguchi; Go Kamoda; Yusuke Matsushita; Chihiro Taguchi; Kohei Suenaga; Masaki Waga; Sho Yokoi

  05 Mar. 2025

  
• Borrowable Fractional Ownership Types for Verification

  Takashi Nakayama; Yusuke Matsushita; Ken Sakayori; Ryosuke Sato; Naoki Kobayashi

  Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, Part II, Jan. 2024, Peer-reviewed

  
• Borrowable Fractional Ownership Types for Verification

  Takashi Nakayama; Yusuke Matsushita; Ken Sakayori; Ryosuke Sato; Naoki Kobayashi

  arXiv, 31 Oct. 2023

  
• RustHornBelt: A semantic foundation for functional verification of Rust programs with unsafe code

  Yusuke Matsushita; Xavier Denis; Jacques-Henri Jourdan; Derek Dreyer

  Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 09 Jun. 2022, Peer-reviewed, Lead author

  
• RustHorn: CHC-based Verification for Rust Programs

  Yusuke Matsushita; Takeshi Tsukada; Naoki Kobayashi

  ACM Transactions on Programming Languages and Systems, 31 Oct. 2021, Peer-reviewed, Invited, Lead author

  
• RustHorn: CHC-Based Verification for Rust Programs

  Yusuke Matsushita; Takeshi Tsukada; Naoki Kobayashi

  Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, 25 Apr. 2020, Peer-reviewed, Lead author

  
• RustHorn: CHC-based Verification for Rust Programs (full version)

  Yusuke Matsushita; Takeshi Tsukada; Naoki Kobayashi

  arXiv, 20 Feb. 2020, Lead author

  

Misc.

• Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows

  Yusuke Matsushita

  Bulletin of Ph.D. Dissertations in AY 2023 Recommended by SIGs, 15 Aug. 2024, Invited, Lead author

  
• Breaking Ground in the World of Software - An Encouragement of Science No.7

  Yusuke Matsushita

  University of Tokyo News from Faculty of Science, 20 May 2022, Invited, Lead author

  

Presentations

• Sciencing the Future of Software—Allured by Rust

  Yusuke Matsushita

  59th Joho-kagaku Wakate-no-kai, 05 Sep. 2026, Invited

  
• Ownership Refinement Types for Pointer Arithmetic and Nested Arrays

  Yusuke Fujiwara; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi

  40th European Conference on Object-Oriented Programming (ECOOP 2026), 01 Jul. 2026

  
• VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System

  Travis Hance; Laila Elbeheiry; Yusuke Matsushita; Derek Dreyer

  Proceedings of the ACM on Programming Languages, 19 Jun. 2026

  
• Pure Borrow: Linear Haskell Meets Rust-Style Borrowing

  Yusuke Matsushita; Hiromi Ishii

  47th ACM SIGPLAN Conference on Programming Language Design and Implementation, 19 Jun. 2026

  
• SoftMatcha 2: Ultra-Fast and Soft Searcher for Trillion-Scale Corpora

  Masataka Yoneda; Go Kamoda; Yusuke Matsushita; Kohei Suenaga; Takuya Akiba; Masaki Waga; Sho Yokoi

  32nd Annual Meeting of the Association for Natural Language Processing (NLP 2026), 10 Mar. 2026

  
• Methods and Implementation of Type-based Rust API Search

  Masayuki Goto; Yusuke Matsushita; Atsushi Igarashi

  28th Workshop on Programming and Programming Languages (PPL 2026), 10 Mar. 2026

  
• Testing Correctness of Unsafe Rust Code Using Dynamic Borrow Checking

  Musashi Katsura; Yusuke Matsushita; Ken Sakayori; Naoki Kobayashi

  28th Workshop on Programming and Programming Languages (PPL 2026), 10 Mar. 2026

  
• Finding Thread-Safety Bugs in Rust Libraries Using Program Synthesis

  Hirotaka Okada; Yusuke Matsushita; Atsushi Igarashi

  28th Workshop on Programming and Programming Languages (PPL 2026), 10 Mar. 2026

  
• A Refinement Type System for Finding Bugs in Functional Language

  Sota Sato; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi

  28th Workshop on Programming and Programming Languages (PPL 2026), 10 Mar. 2026

  
• An Ownership Refinement Type System for Pointer Arithmetic and Nested Arrays

  Yusuke Fujiwara; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi

  28th Workshop on Programming and Programming Languages (PPL 2026), 10 Mar. 2026

  
• RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing

  Yusuke Matsushita; Kengo Hirata; Ryo Wakizaka; Emanuele D'Osualdo

  53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026), 14 Jan. 2026

  
• Nola: Later-Free Ghost State for Verifying Termination in Iris

  Yusuke Matsushita; Takeshi Tsukada

  46th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2025), 20 Jun. 2025

  
• SoftMatcha: A Soft and Fast Pattern Matcher for Billion-Scale Corpus Searches

  Hiroyuki Deguchi; Go Kamoda; Yusuke Matsushita; Chihiro Taguchi; Kohei Suenaga; Masaki Waga; Sho Yokoi

  31st Annual Meeting of the Association for Natural Language Processing (NLP 2025), 13 Mar. 2025

  
• Formally Verifying Imperative Programs with Nested Arrays by Combining Ownership and Refinement Types

  Yusuke Fujiwara; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi

  27th Workshop on Programming and Programming Languages (PPL 2025), 07 Mar. 2025

  
• High-Level Formalization of the C++ Object Model for Memory Safety

  Takashi Nakayama; Yusuke Matsushita; Ken Sakayori; Naoki Kobayashi

  27th Workshop on Programming and Programming Languages (PPL 2025), 05 Mar. 2025

  
• Towards Hyper Hoare Types for Functional Languages

  Sota Sato; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi

  27th Workshop on Programming and Programming Languages (PPL 2025), 05 Mar. 2025

  
• Pure Realization of Rust-Style Borrows in Linear Haskell

  Yusuke Matsushita; Yudai Tanabe; Taro Sekiyama; Atsushi Igarashi

  27th Workshop on Programming and Programming Languages (PPL 2025), 05 Mar. 2025

  
• Concurrent Quantum Separation Logic for Fine-Grained Parallelism

  Yusuke Matsushita; Kengo Hirata; Ryo Wakizaka

  5th International Workshop on Programming Languages for Quantum Computing (PLanQC 2025), 25 Jan. 2025

  
• Concurrent Quantum Separation Logic for Fine-Grained Parallelism

  Yusuke Matsushita; Kengo Hirata; Ryo Wakizaka

  1st Workshop on the Theory and Practice of Static Analysis (TPSA 2025), 21 Jan. 2025

  
• The Fun of Rust

  Yusuke Matsushita

  Colloquium for the Course of CCE, Graduate School of Informatics, Kyoto University, 20 Dec. 2024, Invited

  
• Towards Ownership Refinement Type Inference with Nested Arrays

  Yusuke Fujiwara; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi

  22nd Asian Symposium on Programming Languages and Systems (APLAS 2024) Student Research Competition and Posters, 22 Oct. 2024

  
• The World of Separation Logic Iris

  Yusuke Matsushita

  JSSST PPL Summer School 2024, 09 Sep. 2024, Invited

  
• Towards Soft Grep/KWIC: Making Fast Word Sequence Matching Continuous Using Embedded Representations

  Hiroyuki Deguchi; Go Kamoda; Yusuke Matsushita; Kai Keida; Masaki Waga; Sho Yokoi

  19th Symposium of Young Researcher Association for NLP Studies (YANS 2024), 05 Sep. 2024

  
• New Perspectives on Program Verification and Testing Spreading from Rust

  Yusuke Matsushita

  149th Research Workshop of the Special Interest Group on Programming, Information Processing Society of Japan (PRO-2024-1), 13 Jun. 2024, Invited

  
• Science of Software, Aspiring to a World Free of Bugs

  Yusuke Matsushita; Takashi Nakayama

  Open Campus 2023, the Faculty of Science, the University of Tokyo, 02 Aug. 2023, Invited

  
• Fractional Ownership Type System with Lifetimes for Verifying Imperative Programs

  Takashi Nakayama; Naoki Kobayashi; Ryosuke Sato; Yusuke Matsushita

  25th Workshop on Programming and Programming Languages (PPL 2023), 07 Mar. 2023

  
• RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code

  Yusuke Matsushita; Xavier Denis; Jacques-Henri Jourdan; Derek Dreyer

  43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022), 17 Jun. 2022

  
• RustHorn: CHC-based Verification for Rust Programs

  Yusuke Matsushita; Takeshi Tsukada; Naoki Kobayashi

  29th European Symposium on Programming (ESOP 2020), 31 Mar. 2021

  
• RustHorn: CHC-based Verification for Rust Programs

  Yusuke Matsushita; Takeshi Tsukada; Naoki Kobayashi

  37th Workshop of Japan Society for Software Science and Technology (JSSST 2020), 10 Sep. 2020, Invited

  
• CHC-based Program Verification Exploiting Ownership Types

  Yusuke Matsushita; Naoki Kobayashi; Takeshi Tsukada

  21st Workshop on Programming and Programming Languages (PPL 2019), 06 Mar. 2019

  

Academic, Social Contribution

Committee Memberships

• From Nov. 2025, To Apr. 2026

  PLDI 2026 Review committee member, Association for Computing Machinery (ACM)
• From Jan. 2026, To Mar. 2026

  PPL 2026 Program committee member, Japan Society for Software Science and Technology
• From Jan. 2025, To Mar. 2025

  PPL 2025 Program committee member, Japan Society for Software Science and Technology

Academic Contribution

• External reviewer of ACM PLDI 2025

  Peer review

  From Feb. 2025, To Feb. 2025

  

Social Contribution

• Development Course L1 Rust Verifier Development Seminar Lecturer

  Lecturer

  Information-technology Promotion Agency, Japan, Security Camp 2025 National Conference, From 11 Aug. 2025, To 15 Aug. 2025

  
• Development Course S15 Rust Program Verification Seminar Lecturer

  Lecturer

  Information-technology Promotion Agency, Japan, Security Camp 2024 National Conference, From 12 Aug. 2024, To 16 Aug. 2024