教育研究活動データベース

日本語に切り替えるswitch to english

京都大学の教員等を検索

詳細条件で検索組織別に探す

松下 祐介

マツシタ ユウスケ

白眉センター 特定助教

松下 祐介
list
    Last Updated :2026/10/20

    基本情報

    全学メールアドレス

    • 全学メールアドレス

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

    学位

    • 2021年03月19日
      東京大学修士（情報理工学）
    • 2024年03月21日
      東京大学博士（情報理工学）

    出身大学院・研究科等

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

    出身学校・専攻等

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

    経歴

    • 自 2025年04月, 至 2030年03月
      京都大学, 白眉センター, 特定助教
    • 自 2024年04月, 至 2025年03月
      京都大学, 大学院情報学研究科 通信情報システム専攻, 特定研究員（学振PD）

    ID,URL

    researchmap URL

    list
      Last Updated :2026/10/20

      研究

      研究キーワード

      • 形式検証
      • ソフトウェア科学
      • Rust

      研究分野

      • 情報通信, ソフトウェア, ソフトウェア科学

      論文

      • 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), 2026年08月24日, 査読有り
      • Prophecy-Based Automated Verification of Message-Passing Programs
        Takashi Nagatomi; Musashi Katsura; Naoki Kobayashi; Yusuke Matsushita; Ken Sakayori
        arXiv, 2026年06月26日
      • 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), 2026年06月25日, 査読有り
      • 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, 2026年06月08日, 査読有り
      • Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
        Yusuke Matsushita; Hiromi Ishii
        Proceedings of the ACM on Programming Languages, 2026年06月08日, 査読有り, 筆頭著者
      • 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), 2026年07月06日, 査読有り
      • Ownership Refinement Types for Pointer Arithmetic and Nested Arrays
        Yusuke Fujiwara; Yusuke Matsushita; Kohei Suenaga; Atsushi Igarashi
        arXiv, 2026年04月24日, 筆頭著者
      • Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
        Yusuke Matsushita; Hiromi Ishii
        arXiv, 2026年04月16日, 筆頭著者
      • 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, 2026年02月11日
      • 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, 2026年01月08日, 査読有り, 筆頭著者
      • RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
        Yusuke Matsushita; Kengo Hirata; Ryo Wakizaka; Emanuele D'Osualdo
        arXiv, 2025年11月28日, 筆頭著者
      • Nola: Later-Free Ghost State for Verifying Termination in Iris
        Yusuke Matsushita; Takeshi Tsukada
        Proceedings of the ACM on Programming Languages, 2025年06月13日, 査読有り, 筆頭著者
      • 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), 2025年04月, 査読有り
      • 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
        2025年03月05日
      • 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, 2024年01月, 査読有り
      • Borrowable Fractional Ownership Types for Verification
        Takashi Nakayama; Yusuke Matsushita; Ken Sakayori; Ryosuke Sato; Naoki Kobayashi
        arXiv, 2023年10月31日
      • 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, 2022年06月09日, 査読有り, 筆頭著者
      • RustHorn: CHC-based Verification for Rust Programs
        Yusuke Matsushita; Takeshi Tsukada; Naoki Kobayashi
        ACM Transactions on Programming Languages and Systems, 2021年10月31日, 査読有り, 招待有り, 筆頭著者
      • RustHorn: CHC-Based Verification for Rust Programs
        Yusuke Matsushita; Takeshi Tsukada; Naoki Kobayashi
        Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, 2020年04月25日, 査読有り, 筆頭著者
      • RustHorn: CHC-based Verification for Rust Programs (full version)
        Yusuke Matsushita; Takeshi Tsukada; Naoki Kobayashi
        arXiv, 2020年02月20日, 筆頭著者

      MISC

      • Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows
        松下 祐介
        2023 年度研究会推薦博士論文速報, 2024年08月15日, 招待有り, 筆頭著者
      • ソフトウェアの世界を切り拓く - 理学のススメ No.7
        松下 祐介
        東京大学 理学部ニュース, 2022年05月20日, 招待有り, 筆頭著者

      講演・口頭発表等

      • ソフトウェアの未来を科学する——Rust に誘われて
        松下 祐介
        第59回 情報科学若手の会, 2026年09月05日, 招待有り
      • 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), 2026年07月01日
      • 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, 2026年06月19日
      • Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
        Yusuke Matsushita; Hiromi Ishii
        47th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2026年06月19日
      • SoftMatcha 2: 1兆語規模コーパスの超高速かつ柔らかい検索
        米田 優峻; 鴨田 豪; 松下 祐介; 末永 幸平; 秋葉 拓哉; 和賀 正樹; 横井 祥
        言語処理学会第32回年次大会 (NLP 2026), 2026年03月10日
      • 型に基づくRust API探索の手法と実装
        後藤 将之; 松下 祐介; 五十嵐 淳
        第28回プログラミングおよびプログラミング言語ワークショップ (PPL 2026), 2026年03月10日
      • 動的な借用検査を活用したUnsafe Rustコードの正当性検査
        桂 武蔵; 松下 祐介; 小林 直樹; 酒寄 健
        第28回プログラミングおよびプログラミング言語ワークショップ (PPL 2026), 2026年03月10日
      • Rustライブラリのスレッド安全性に関するバグのプログラム合成による発見
        岡田 大空; 松下 祐介; 五十嵐 淳
        第28回プログラミングおよびプログラミング言語ワークショップ (PPL 2026), 2026年03月10日
      • 関数型言語のバグ発見のための篩型システム
        佐藤 聡太; 松下 祐介; 末永 幸平; 五十嵐 淳
        第28回プログラミングおよびプログラミング言語ワークショップ (PPL 2026), 2026年03月10日
      • ポインタ演算と多次元配列のための所有権篩型システム
        藤原 佑輔; 松下 祐介; 末永 幸平; 五十嵐 淳
        第28回プログラミングおよびプログラミング言語ワークショップ (PPL 2026), 2026年03月10日
      • 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), 2026年01月14日
      • 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), 2025年06月20日
      • SoftMatcha: 大規模コーパス検索のための柔らかくも高速なパターンマッチャー
        出口 祥之; 鴨田 豪; 松下 祐介; 田口 智大; 末永 幸平; 和賀 正樹; 横井 祥
        言語処理学会第31回年次大会 (NLP 2025), 2025年03月13日
      • 多重配列を扱う命令型プログラムの所有権と篩型の組み合わせによる形式検証
        藤原 佑輔; 松下 祐介; 末永 幸平; 五十嵐 淳
        第27回プログラミングおよびプログラミング言語ワークショップ (PPL 2025), 2025年03月07日
      • メモリ安全性のためのC++オブジェクトモデルのハイレベルな形式化
        中山 崇; 松下 祐介; 酒寄 健; 小林 直樹
        第27回プログラミングおよびプログラミング言語ワークショップ (PPL 2025), 2025年03月05日
      • 関数型言語のためのHyper Hoare Typeにむけて
        佐藤 聡太; 松下 祐介; 末永 幸平; 五十嵐 淳
        第27回プログラミングおよびプログラミング言語ワークショップ (PPL 2025), 2025年03月05日
      • Linear Haskell での Rust 流借用の純粋な実現
        松下 祐介; 田邉 裕大; 関山 太朗; 五十嵐 淳
        第27回プログラミングおよびプログラミング言語ワークショップ (PPL 2025), 2025年03月05日
      • 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), 2025年01月25日
      • 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), 2025年01月21日
      • Rust の面白さ
        松下 祐介
        京都大学 大学院情報学研究科 通信情報システムコース 談話会, 2024年12月20日, 招待有り
      • 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, 2024年10月22日
      • 分離論理 Iris の世界
        松下 祐介
        JSSST PPL サマースクール 2024, 2024年09月09日, 招待有り
      • 柔らかいgrep/KWICに向けて：高速単語列マッチングの埋め込み表現による連続化
        出口 祥之; 鴨田 豪; 松下 祐介; 慶田 開; 和賀 正樹; 横井 祥
        第19回言語処理若手シンポジウム (YANS 2024), 2024年09月05日
      • Rust から広がるプログラム検証・テストの新展望
        松下 祐介
        情報処理学会 第149回プログラミング研究発表会 (PRO-2024-1), 2024年06月13日, 招待有り
      • ソフトウェアの科学 〜バグのない世界を目指して〜
        松下 祐介; 中山 崇
        東京大学理学部オープンキャンパス, 2023年08月02日, 招待有り
      • 命令型プログラムの検証のためのライフタイム付き分数所有権型システム
        中山 崇; 小林 直樹; 佐藤 亮介; 松下 祐介
        第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 2023年03月07日
      • 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), 2022年06月17日
      • RustHorn: CHC-based Verification for Rust Programs
        Yusuke Matsushita; Takeshi Tsukada; Naoki Kobayashi
        29th European Symposium on Programming (ESOP 2020), 2021年03月31日
      • RustHorn: CHC-based Verification for Rust Programs
        松下 祐介; 塚田 武志; 小林 直樹
        日本ソフトウェア科学会第37回大会 (JSSST 2020), 2020年09月10日, 招待有り
      • 所有権型を利用した CHC ベースのプログラム検証
        松下 祐介; 小林 直樹; 塚田 武志
        第21回プログラミングおよびプログラミング言語ワークショップ (PPL 2019), 2019年03月06日
      list
        Last Updated :2026/10/20

        学術・社会貢献

        委員歴

        • 自 2025年11月, 至 2026年04月
          PLDI 2026 Review committee member, Association for Computing Machinery (ACM)
        • 自 2026年01月, 至 2026年03月
          PPL 2026 プログラム委員, 日本ソフトウェア科学会
        • 自 2025年01月, 至 2025年03月
          PPL 2025 プログラム委員, 日本ソフトウェア科学会

        学術貢献活動

        • ACM PLDI 2025 外部査読者
          査読
          自 2025年02月, 至 2025年02月

        社会貢献活動

        • 開発コース L1 Rust 検証器自作ゼミ 講師
          講師
          情報処理推進機構, セキュリティ・キャンプ 2025 全国大会, 自 2025年08月11日, 至 2025年08月15日
        • 開発コース S15 Rust プログラム検証ゼミ 講師
          講師
          情報処理推進機構, セキュリティ・キャンプ 2024 全国大会, 自 2024年08月12日, 至 2024年08月16日

        ページ上部へ戻る