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

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

末永 幸平

スエナガ コウヘイ

情報学研究科 通信情報システム専攻コンピュータ工学講座 准教授

末永 幸平
list
    Last Updated :2022/11/23

    基本情報

    学部兼担

    • 工学部 工学部

    所属学協会

    • IPSJ
    • JSSST
    • ACM

    学位

    • 修士(情報理工学)(東京大学)
    • 博士(情報理工学)(東京大学)

    出身大学院・研究科等

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

    出身学校・専攻等

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

    出身高等学校

    • 出身高等学校

      宮崎県立宮崎西高等学校, みやざきけんりつみやざきにしこうとうがっこう

    経歴

    • 自 2019年09月, 至 現在
      一般社団法人 社会システムデザインセンター, アドバイザー
    • 自 2019年05月, 至 現在
      株式会社センスタイムジャパン, 技術顧問
    • 自 2019年05月, 至 現在
      ダイラムダ株式会社, 技術顧問
    • 自 2017年06月, 至 現在
      Patentfield 株式会社, 科学技術顧問
    • 自 2017年04月, 至 現在
      LegalForce Inc., 技術顧問
    • 自 2013年10月, 至 現在
      京都大学, 大学院情報学研究科, 准教授
    • 自 2015年10月, 至 2019年03月
      科学技術振興機構さきがけ, 兼任研究員
    • 自 2012年04月, 至 2013年09月
      京都大学, 白眉センター, 特定助教
    • 自 2011年04月, 至 2012年03月
      日本学術振興会, 特別研究員 (PD)
    • 自 2011年02月, 至 2011年03月
      京都大学, 大学院情報学研究科, 特定研究員
    • 自 2010年04月, 至 2011年01月
      リスボン大学, 理学部, 博士研究員
    • 自 2009年04月, 至 2010年03月
      日本アイ・ビー・エム株式会社, 東京基礎研究所, リサーチャー
    • 自 2008年04月, 至 2009年03月
      日本学術振興会, 特別研究員 (PD)
    • 自 2007年04月, 至 2008年03月
      日本学術振興会, 特別研究員 (DC2)

    プロフィール

    • プロフィール

      2008年東京大学情報理工学系研究科コンピュータ科学専攻修了.博士(情報理工学).日本学術振興会特別研究員 (DC2, PD),日本アイ・ビー・エム(株)東京基礎研究所リサーチャー,リスボン大学理学部博士研究員,日本学術振興会特別研究員 (PD),京都大学白眉センター特定助教,を経て 2013年より京都大学大学院情報学研究科准教授.現在に至る.2018年より国立情報学研究所客員准教授.ソフトウェアシステム,ハイブリッドシステム,機械学習システム,スマートコントラクトの形式検証手法に興味を持つ.


      異なる分野で使われている手法を形式検証の分野に持ち込んだり,形式検証のアイデアを他の分野に持ち込んだりするのが好きです.色んな分野の人と話をするのが好きです.

    使用言語

    • 英語
    • ポルトガル語

    ID,URL

    researchmap URL

    list
      Last Updated :2022/11/23

      研究

      研究テーマ・研究概要

      • 研究テーマ

        形式検証手法
      • 研究概要

        さまざまなシステムのための形式検証手法を研究しています.形式検証とは,数学を用いてシステムのバグを発見したり,システムにバグが存在しないことを証明したりするための手法です.もともとハードウェアを検査するための手法として提案された手法ですが,コンピュータが社会の様々なところで用いられるに従って,ソフトウェアを検証するための手法としても広く用いられるようになっています.また近年では,伝統的なソフトウェアに限らず,ハイブリッドシステム(プログラムと微分方程式との組み合わせで記述されるシステム)や機械学習システム等,検証が必要なシステムの種類が増えてきています.

        末永はプログラミング言語理論に関する専門的知見をコアとして,この知見を様々なシステムに適用するための研究を行っています.最近はハイブリッドシステム,スマートコントラクト,機械学習システムの検証手法を研究しています.もちろん,普通のソフトウェアに適用可能な手法も研究しています.

      研究キーワード

      • 静的検証
      • 超準解析
      • 形式手法
      • 型システム
      • ホーア論理
      • プログラミング言語
      • 無限小プログラミング
      • ハイブリッドシステム

      研究分野

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

      論文

      • Sound and Relatively Complete Belief Hoare Logic for Statistical Hypothesis Testing Programs.
        Yusuke Kawamoto 0001; Tetsuya Sato 0001; Kohei Suenaga
        CoRR, 2022年
      • SCameleer: スマートコントラクト記述言語SCamlのための自動検証器
        服部 佑哉; 西田 雄気; 古瀬 淳; 末永 幸平; 五十嵐 淳
        日本ソフトウェア科学会 第39回大会講演論文集, 2022年09月
      • スマートコントラクト検証器Helmholtzのためのエラー原因提示手法
        小野 雄登; 西田 雄気; 古瀬 淳; 末永 幸平; 五十嵐 淳
        日本ソフトウェア科学会 第39回大会講演論文集, 2022年09月
      • Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption.
        Ryotaro Banno; Kotaro Matsuoka; Naoki Matsumoto; Song Bian; Masaki Waga; Kohei Suenaga
        CAV 2022, 2022年, 査読有り
      • The Lattice-Theoretic Essence of Property Directed Reachability Analysis.
        Mayuko Kori; Natsuki Urabe; Shin-ya Katsumata; Kohei Suenaga; Ichiro Hasuo
        CAV 2022, 2022年, 査読有り
      • Goal-Aware RSS for Complex Scenarios via Program Logic.
        Ichiro Hasuo; Clovis Eberhart; James Haydon; Jérémy Dubut; Rose Bohrer; Tsutomu Kobayashi; Sasinee Pruekprasert; Xiao-Yi Zhang; Erik André Pallas; Akihisa Yamada 0002; Kohei Suenaga; Fuyuki Ishikawa; Kenji Kamijo; Yoshiyuki Shinya; Takamasa Suetomi
        CoRR, 2022年
      • Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption.
        Ryotaro Banno; Kotaro Matsuoka; Naoki Matsumoto; Song Bian 0001; Masaki Waga; Kohei Suenaga
        CoRR, 2022年
      • The Lattice-Theoretic Essence of PropertyDirected Reachability Analysis.
        Mayuko Kori; Natsuki Urabe; Shin-ya Katsumata; Kohei Suenaga; Ichiro Hasuo
        CoRR, 2022年
      • Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types.
        Yuki Nishida 0001; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi
        Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, 2021年, 査読有り
      • Ordered Types for Stream Processing of Tree-Structured Data
        Sato Ryosuke; Suenaga Kohei; Kobayashi Naoki
        Information and Media Technologies, 2011年
      • 完全準同型暗号を用いた秘匿LTLオンラインモニタリング
        伴野 良太郎; 松岡 航太郎; 松本 直樹; Bian Song; 和賀 正樹; 末永 幸平
        コンピュータセキュリティシンポジウム 2021 (CSS 2021), 2021年10月, 最終著者
      • Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic.
        Yusuke Kawamoto; Tetsuya Sato; Kohei Suenaga
        Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning(KR), 2021年, 査読有り
      • Efficient Black-Box Checking via Model Checking with Strengthened Specifications
        Junya Shijubo; Masaki Waga; Kohei Suenaga
        Runtime Verification - 21st International Conference(RV), 2021年, 査読有り, 最終著者
      • Enhancing Loop-Invariant Synthesis via Reinforcement Learning.
        Takeshi Tsukada; Hiroshi Unno 0001; Taro Sekiyama; Kohei Suenaga
        CoRR, 2021年
      • Verification of a Merkle Patricia Tree Library Using F.
        Sota Sato; Ryotaro Banno; Jun Furuse; Kohei Suenaga; Atsushi Igarashi
        CoRR, 2021年
      • Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs.
        Ichiro Hasuo; Yuichiro Oyabu; Clovis Eberhart; Kohei Suenaga; Kenta Cho 0002; Shin-ya Katsumata
        CoRR, 2021年
      • Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
        Yuki Nishida; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi
        New Generation Computing, 2022年05月27日, 査読有り
      • スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証
        齋藤 大聖; 西田 雄気; 五十嵐 淳; 末永 幸平
        PPL 2020, 2020年03月, 査読有り
      • F*を用いたMerkle Patricia Treeライブラリの形式検証
        佐藤 聡太; 古瀬 淳; 末永 幸平; 五十嵐 淳
        PPL 2020, 2020年03月, 査読有り
      • Visualizing Color-Wise Saliency of Black-Box Image Classification Models.
        Yuhki Hatakeyama; Hiroki Sakuma; Yoshinori Konishi; Kohei Suenaga
        Proceedings of ACCV 2020, 2020年, 査読有り
      • Generalized Property-Directed Reachability for Hybrid Systems
        Kohei Suenaga; Takuya Ishizawa
        Verification, Model Checking, and Abstract Interpretation - 21st International Conference(VMCAI), 2020年, 査読有り
      • A Contract Corpus for Recognizing Rights and Obligations.
        Ruka Funaki; Yusuke Nagata; Kohei Suenaga; Shinsuke Mori
        Proceedings of The 12th Language Resources and Evaluation Conference(LREC), 2020年, 査読有り
      • ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
        John Toman; Ren Siqi; Kohei Suenaga; Atsushi Igarashi; Naoki Kobayashi
        29th European Symposium on Programming (ESOP 2020), 2020年, 査読有り
      • Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks
        Taro Sekiyama; Kohei Suenaga
        APLAS 2018, 2018年, 査読有り
      • A guess-and-assume approach to loop fusion for program verification.
        Akifumi Imanishi; Kohei Suenaga; Atsushi Igarashi
        PEPM 2018, 2018年, 査読有り
      • Automated proof synthesis for propositional logic with deep neural networks.
        Taro Sekiyama; Kohei Suenaga
        CoRR, 2018年
      • MONAA: A Tool for Timed Pattern Matching with Automata-Based Acceleration.
        Masaki Waga; Ichiro Hasuo; Kohei Suenaga
        3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, 2018年, 査読有り
      • Generalized homogeneous polynomials for efficient template-based nonlinear invariant synthesis.
        Kensuke Kojima; Minoru Kinoshita; Kohei Suenaga
        Theor. Comput. Sci., 2018年, 査読有り
      • Sharper and Simpler Nonlinear Interpolants for Program Verification
        Takamasa Okudono; Yuki Nishida; Kensuke Kojima; Kohei Suenaga; Kengo Kido; Ichiro Hasuo
        Programming Languages and Systems (APLAS 2017), 2017年, 査読有り
      • A Nonstandard Functional Programming Language
        Hirofumi Nakamura; Kensuke Kojima; Kohei Suenaga; Atsushi Igarashi
        Programming Languages and Systems (APLAS 2017), 2017年, 査読有り
      • Efficient Online Timed Pattern Matching by Automata-Based Skipping
        Masaki Waga; Ichiro Hasuo; Kohei Suenaga
        FORMATS 2017, 2017年, 査読有り
      • Towards Proof Synthesis Guided by Neural Machine Translation for Intuitionistic Propositional Logic
        Taro Sekiyama; Akifumi Imanishi; Kohei Suenaga
        CoRR, 2017年, 査読有り
      • An Extended Behavioral Type System for Memory-Leak Freedom
        Qi Tan; Kohei Suenaga; Atsushi Igarashi
        日本ソフトウェア科学会第33回大会論文集, 2016年09月
      • Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis.
        Kensuke Kojima; Minoru Kinoshita; Kohei Suenaga
        STATIC ANALYSIS, (SAS 2016), 2016年, 査読有り
      • Input Synthesis for Sampled Data Systems by Program Logic
        Takumi Akazaki; Ichiro Hasuo; Kohei Suenaga
        Proc. of the 4th Workshop on Hybrid Autonomous Systems (HAS 2014), 2015年01月24日, 査読有り
      • Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).
        Daisuke Ishii; Kohei Suenaga; Walid Taha
        NII Shonan Meet. Rep., 2015年
      • Automatic Memory Management Based on Program Transformation Using Ownership.
        Tatsuya Sonobe; Kohei Suenaga; Atsushi Igarashi
        Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, 2014年, 査読有り
      • Hyperstream processing systems: Nonstandard modeling of continuous-time signals
        Kohei Suenaga; Hiroyoshi Sekine; Ichiro Hasuo
        Conference Record of the Annual ACM Symposium on Principles of Programming Languages, 2013年, 査読有り
      • Type-based safe resource deallocation for shared-memory concurrency
        Kohei Suenaga; Ryota Fukuda; Atsushi Igarashi
        Proceedings of OOPSLA 2021, 2012年10月, 査読有り
      • Exercises in Nonstandard Static Analysis of Hybrid Systems
        Ichiro Hasuo; Kohei Suenaga
        24th International Conference, CAV 2012, 2012年, 査読有り
      • Ordered Types for Stream Processing of Tree-Structured Data
        Ryosuke Sato; Kohei Suenaga; Naoki Kobayashi
        JIP, 2011年, 査読有り
      • Programming with Infinitesimals: A WHILE-Language for Hybrid System Modeling
        Kohei Suenaga; Ichiro Hasuo
        Automata, Languages and Programming, ICALP, Pt II, 2011年, 査読有り
      • RA-010 Ordered Types for Stream Processing of Tree-Structured Data
        佐藤 亮介; 末永 幸平; 小林 直樹
        情報科学技術フォーラム講演論文集, 2009年08月20日
      • Fractional Ownerships for Safe Memory Deallocation
        Kohei Suenaga; Naoki Kobayashi
        7th Asian Symposium, APLAS 2009, 2009年, 査読有り
      • 型エラースライシングによるデッドロックの原因特定
        飯村 枝里; 小林 直樹; 末永 幸平
        情報処理学会論文誌プログラミング(PRO), 2008年09月26日
      • Type-Based Deadlock-Freedom Verification for Non-Block-Structured Lock Primitives and Mutable References
        Kohei Suenaga
        6th Asian Symposium, APLAS 2008, 2008年, 査読有り, 筆頭著者
      • Translation of tree-processing programs into stream-processing programs based on ordered linear type
        Koichi Kodama; Kohei Suenaga; Naoki Kobayashi
        J. Funct. Program., 2008年, 査読有り
      • Type-based analysis of deadlock for a concurrent calculus with interrupts
        Kohei Suenaga; Naoki Kobayashi
        ESOP'07: Proceedings of the 16th European Symposium on Programming, 2007年, 査読有り
      • Extension of type-based approach to generation of stream-processing programs by automatic insertion of buffering primitives
        Kohei Suenaga; Naoki Kobayashi; Akinori Yonezawa
        LOPSTR'05: Proceedings of the 15th international conference on Logic Based Program Synthesis and Transformation, 2006年, 査読有り
      • Resource usage analysis for the pi-calculus
        N Kobayashi; K Suenaga; L Wischik
        7th International Conference, VMCAI 2006, 2006年, 査読有り
      • Resource Usage Analysis for the Pi-Calculus
        Naoki Kobayashi; Kohei Suenaga; Lucian Wischik
        Logical Methods in Computer Science, 2006年, 査読有り
      • The Interface Definition Language for Fail-Safe C
        K Suenaga; Y Oiwa; E Sumii; A Yonezawa
        SOFTWARE SECURITY - THEORIES AND SYSTEMS, 2004年, 査読有り
      • Translation of tree-processing programs into stream-processing programs based on ordered linear type
        K Kodama; K Suenaga; N Kobayashi
        PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2004年, 査読有り
      • Fail-Safe Cのためのインターフェイス定義言語
        末永幸平; 大岩寛; 住井英二郎; 米澤明憲
        第5回プログラミングおよびプログラミング言語ワークショップ(PPL 2003)論文集, 2003年, 査読有り
      • CPSの形式検証——超準解析によるアプローチ
        蓮尾 一郎; 末永 幸平
        計測と制御, 2014年

      MISC

      • 昔のネタ帳から
        末永幸平
        コンピュータソフトウェア, 2022年04月, 招待有り
      • PLDI 2016参加報告
        末永 幸平
        コンピュータソフトウェア = Computer software, 2017年02月, 招待有り

      講演・口頭発表等

      • Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
        Kohei Suenaga
        US-Japan Seminar on Autonomy AI, Robotics, and Informatics, 2022年10月11日, 招待有り
      • JST CREST 研究課題「AI 集約的サイバーフィジカルシステムの形式的解析設計手法」の概観と研究成果の紹介
        末永幸平
        2022年電子情報通信学会ソサイエティ大会企画セッション「 AI を含むサイバーフィジカルシステムの背景技術 〜信頼性向上を⽬指して〜」, 2022年09月06日, 招待有り
      • SCameleer: スマートコントラクト記述言語SCamlのための自動検証器
        服部 佑哉; 西田 雄気; 古瀬 淳; 末永 幸平; 五十嵐 淳
        日本ソフトウェア科学会第39回大会, 2022年09月02日
      • スマートコントラクト検証器Helmholtzのためのエラー原因提示手法
        小野 雄登; 西田 雄気; 古瀬 淳; 末永 幸平; 五十嵐 淳
        日本ソフトウェア科学会第39回大会, 2022年09月01日
      • Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
        Ryotaro Banno; Kotaro Matsuoka; Naoki Matsumoto; Song Bian; Masaki Waga; Kohei Suenaga
        CAV 2022, 2022年08月
      • The Lattice-Theoretic Essence of Property Directed Reachability Analysis
        Mayuko Kori; Natsuki Urabe; Shin-ya Katsumata; Kohei Suenaga; Ichiro Hasuo
        CAV 2022, 2022年08月
      • 物理情報システムに対するブラックボックス検査の構文的仕様強化による最適化
        四十坊純也; 和賀正樹; 末永幸平
        第23回プログラミングおよびプログラミング言語ワークショップ (PPL 2021), 2021年03月10日
      • 暗号通貨向けストレージシステムにおけるデータ永続化処理の形式検証
        伴野良太郎; 佐藤聡太; 古瀬淳; 末永幸平; 五十嵐淳
        第23回プログラミングおよびプログラミング言語ワークショップ (PPL 2021), 2021年03月09日
      • Visualizing Color-Wise Saliency of Black-Box Image Classification Models
        Yuhki Hatakeyama; Hiroki Sakuma; Yoshinori Konishi; Kohei Suenaga
        ACCV 2020
      • ブラックボックス画像分類モデルの否定的判断根拠と色情報根拠の可視化
        畠山雄気; 佐久間宏樹; 小西嘉典; 末永幸平
        MIRU 2020
      • F*を用いたMerkle Patricia Treeライブラリの形式検証
        佐藤 聡太; 古瀬 淳; 末永 幸平; 五十嵐 淳
        PPL 2020
      • スマートコントラクトのための Effectively Callback-Free 性の型に基づく静的検証
        齋藤 大聖; 西田 雄気; 五十嵐 淳; 末永 幸平
        PPL 2020
      • Generalized Property-Directed Reachability for Hybrid Systems
        Kohei Suenaga; Takuya Ishizawa
        VMCAI 2020, 2020年01月19日
      • Automated proof synthesis for propositional logic using deep learning
        Kohei Suenaga
        5th France-Japan Cybersecurity workshop, 2019年04月23日, 招待有り
      • 日本語契約書の一般的な構造定義に向けて
        舟木類佳; 末永幸平; 森信介
        2019年03月13日
      • Automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks
        Taro Sekiyama; Kohei Suenaga
        APLAS 2018, 2018年12月03日
      • Property-Directed Reachability for Hybrid Systems with Differential Dynamic Logic Predicates
        Takuya Ishizawa; Kohei Suenaga
        APLAS 2018 Student Research Competition, 2018年12月02日
      • ニューラルネットワークによるフォトニック結晶格子点構造の3次元モデリングの検討
        田上 智基; 北村 恭子; 末永 幸平; 石崎 賢司; 野田 進
        第65回応用物理学会春季学術講演会, 2018年03月20日
      • Towards Proof Synthesis by Neural Machine Translation
        Taro Sekiyama; Akifumi Imanishi; Kohei Suenaga
        Off the Beaten Track 2018 (OBT 2018), 2018年01月13日
      • A Guess-and-Assume Approach to Loop Fusion for Program Verification
        Akifumi Imanishi; Kohei Suenaga; Atsushi Igarashi
        PEPM 2018, 2018年01月07日
      • 超準プログラミング言語を用いたハイブリッドシステムのモデリングと検証
        末永 幸平
        第9回 暗号及び情報セキュリティと数学の相関ワークショップ (CRISMATH 2017), 2017年12月22日, 招待有り
      • A Nonstandard Functional Programming Language
        Hirofumi Nakamura; Kensuke Kojima; Kohei Suenaga; Atsushi Igarashi
        APLAS 2017, 2017年11月27日
      • Sharper and Simpler Nonlinear Interpolants for Program Verification
        Takamasa Okudono; Yuki Nishida; Kensuke Kojima; Kohei Suenaga; Kengo Kido; Ichiro Hasuo
        APLAS 2017, 2017年11月27日
      • Efficient Online Timed Pattern Matching by Automata-Based Skipping
        Masaki Waga; Ichiro Hasuo; Kohei Suenaga
        15th International Conference on Formal Modelling and Analysis of Timed Systems, 2017年09月05日
      • Sharper and Simpler Nonlinear Interpolants for Program Verification
        Takamasa Okudono; Yuki Nishida; Kensuke Kojima; Kohei Suenaga; Kengo Kido; Ichiro Hasuo
        Workshop on Formal Approaches to Explainable VERification (FEVER 2017), 2017年07月23日
      • 超準関数型プログラミング言語NSF
        中村 博文; 末永 幸平; 五十嵐 淳; 小島 健介
        第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017), 2017年03月08日
      • 深層学習によるプログラム生成の高速化
        今西 諒文; 関山 太朗; 村主 崇行; 末永 幸平
        第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017), 2017年03月08日
      • 無限状態システムのHFLモデル検査のための型に基づく手法
        今井 雄毅; 小林 直樹; 佐藤 亮介; 末永 幸平; 塚田 武志
        第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017), 2017年03月08日
      • Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis
        Kensuke Kojima; Minoru Kinoshita; Kohei Suenaga
        第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017), 2017年03月08日
      • 超準解析を用いたハイブリッドシステム検証手法
        末永 幸平
        統計数理解析研究所シンポジウム --- 工学と現代数学の接点を求めて, 2016年12月20日, 招待有り
      • Generalized Homogeneous Polynomials for Efficient Template-Based Nonlinear Invariant Synthesis
        末永 幸平
        SAS 2016, 2016年09月08日
      • An Extended Behavioral Type System for Memory-Leak Freedom
        Qi Tan; Kohei Suenaga; Atsushi Igarashi
        日本ソフトウェア科学会 第33回大会講演論文集, 2016年09月07日
      • ソフトウェアのための自動形式検証ツール
        末永 幸平
        ET/IoT 総合技術展 関西(ETWest 2016), 2016年07月07日
      • Formal verification of software, continuous, and hybrid systems -- Or: How do we verify our program is correct?
        末永 幸平
        Machine Learning Summer School 2015, 2015年08月27日
      • Nonstandard Analysis Meets Programming Language Theory
        末永 幸平
        Twelfth International Conference on Computability and Complexity in Analysis, 2015年07月13日, 招待有り
      • Automatic Synthesis of Combiners in the MapReduce Framework
        樹下 稔; 末永 幸平; 五十嵐 淳
        24th International Symposium on Logic-Based Program Synthesis and Transformation, 2014年09月09日
      • Type-Based Safe Resource Deallocation for Shared-Memory Concurrency
        末永 幸平
        日本ソフトウェア科学会第30回大会特別招待講演, 2013年09月12日, 招待有り
      • 形式検証手法は無限小プログラミングを使えばハイブリッドシステムにもそのまま使える
        末永 幸平
        日本ソフトウェア科学会第30回大会Future Technology Design (FTD) 2013, 2013年09月11日, 招待有り
      • Simulink blocks as stream processing ─ An approach from nonstandard analysis (Preliminary Report)
        関根 大剛; 末永 幸平; 蓮尾 一郎
        Fifth International Workshop on Numerical Software Verification (NSV 2012), 2012年07月07日
      • 京都大学 Teen Racketeer 養成コース
        五十嵐 淳; 中澤 巧爾; 馬谷 誠二; 関山 太朗; 花田 裕一朗; 大元 武; 宮本 洋平; 末永 幸平
        第17回プログラミングおよびプログラミング言語ワークショップ, 2015年03月05日
      • The Lattice-Theoretic Essence of Property Directed Reachability Analysis
        Mayuko Kori; Natsuki Urabe; Shin-ya Katsumata; Kohei Suenaga; Ichiro Hasuo
        16th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2022), 2022年04月03日
      • Regnant: 分割可能所有権と篩型を用いた Java 検証器
        小林 亮太; John Toman; 五十嵐 淳; 末永 幸平
        第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022), 2022年03月08日
      • Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types
        Yuki Nishida; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi
        第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022), 2022年03月06日

      書籍等出版物

      • 理論計算機科学事典
        徳山, 豪; 小林, 直樹; 岩間, 一雄; 渡辺, 治; 今井, 浩; 南出, 靖彦; 五十嵐, 淳; 長谷川, 真人, 8.3節「型に基づくプログラム検証」
        朝倉書店, 2022年01月

      産業財産権

      • 特願2021-180647, 情報処理装置、情報処理方法および情報処理プログラム
        菊池淳; 和賀正樹; 末永幸平
      • 特許6910228, 特開2019-020966, 特願2017-137949, 自動証明装置、及びプログラム
        蓮尾 一郎; 奥殿 貴仁; 木戸 肩吾; 末永 幸平; 小島 健介; 西田 雄気
      • PCT/JP2018/044029, プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、 プログラム変換器、プログラム変換方 法、プログラム変換のためのコンピュータプログラム、 プログラム製造方法、及び検証用プログラム
        末永 幸平; 今西 諒文; 五十嵐 淳
      • 特願2017-246154, プログラム検証装置、プログラム検証方法、プログラム検証のためのコンピュータプログラム、プログラム変換器、プログラム変換方法、プログラム変換のためのコンピュータプログラム、プログラム製造方法、及び検証用プログラム
        末永 幸平; 今西 諒文; 五十嵐 淳
      • 特許6632058, 特開2017-138679, 特願2016-017441, 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法
        末永 幸平; 樹下 稔; 小島 健介
      • 特許6622098, 特開2017-138677, 特願2016-017419, 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法
        末永 幸平; 樹下 稔; 小島 健介
      • PCT/JP2017/003295, 不変条件生成装置、コンピュータプログラム、不変条件生成方法、プログラムコード製造方法
        樹下稔; 小島健介; 末永幸平
      • 特許第5843230号, 特開2013-003897, 特願2011-135201, ハイブリッドシステムの検証方法、検証装置、及び検証コンピュータプログラム、並びに、ハイブリッドシステムのモデル変換方法、変換装置、及び変換コンピュータプログラム
        末永 幸平; 蓮尾 一郎
      • 特開2015-194917, 特願2014-072623, 制御入力値生成装置、制御入力値生成方法、および、プログラム
        蓮尾 一郎; 赤崎 拓未; 末永 幸平
      • 特願2014-72623, 制御入力値生成装置,制御入力値生成方法,および,プログラム
        赤崎 拓未; 蓮尾 一郎; 末永 幸平
      • 特許第5431261号, 特開2012-027685, 特願2010-165620, 情報管理システム、方法及びプログラム
        中村 宏明; 宮下 尚; 末永 幸平

      受賞

      • 2007年03月
        日本ソフトウェア科学会プログラミング論研究会, PPL 2007 発表賞
      • 2009年03月
        日本ソフトウェア科学会プログラミング論研究会, PPL 2009 発表賞
      • 2012年03月
        日本ソフトウェア科学会プログラミング論研究会, PPL 2012 発表賞
      • 2012年06月
        情報処理学会, Journal of Information Processing Outstanding Paper Award
      • 2013年09月
        京都大学, 京都大学学際研究着想コンテスト優秀賞

      外部資金:科学研究費補助金

      • 高相互運用性を持つソフトウェアモジュールのためのソフトウェア契約の研究
        基盤研究(A)
        中区分60:情報科学、情報工学およびその関連分野
        京都大学
        五十嵐 淳
        自 2020年04月01日, 至 2025年03月31日, 交付
        プログラミング言語;プログラム検証;相互運用性;ソフトウェア契約;ソフトウエア契約
      • 数学の自動化を推進するための機械学習を用いた定理自動証明手法
        挑戦的研究(萌芽)
        中区分60:情報科学、情報工学およびその関連分野
        京都大学
        末永 幸平
        自 2019年06月28日, 至 2022年03月31日, 交付
        機械学習;定理証明;強化学習;ホーン節ソルバ;人工知能;自動証明;深層学習
      • IoT システムのための形式検証手法の深化
        基盤研究(B)
        小区分60050:ソフトウェア関連
        京都大学
        末永 幸平
        自 2019年04月01日, 至 2024年03月31日, 交付
        プログラム検証;形式検証;IoT;モデル検査;ハイブリッドシステム;強化学習;機械学習;形式手法
      • 圏論と数理論理学によるものづくりサポート―ソフトウェア科学のシステム工学への移転
        基盤研究(B)
        国立情報学研究所;東京大学
        蓮尾 一郎
        自 2015年07月10日, 至 2020年03月31日, 完了
        物理情報システム;形式検証;テスト;ハイブリッドシステム;数理論理学;統計的機械学習;圏論;プログラム理論;モデルベース開発;不動点論理
      • 無限小プログラミングによるハイブリッドシステムの形式検証手法
        若手研究(B)
        京都大学
        末永 幸平
        自 2013年04月01日, 至 2016年03月31日, 完了
        ハイブリッドシステム;プログラム検証;不変条件;無限小プログラミング;超準解析;次元解析;非線形不変条件;システム検証;形式手法;形式検証;プログラミング言語;プログラミング言語理論;プログラム意味論;プログラム理論
      • ソフトウェア契約に基づく高階型付プログラムの理論
        基盤研究(B)
        京都大学
        五十嵐 淳
        自 2013年04月01日, 至 2017年03月31日, 完了
        プログラミング言語;ソフトウェア契約;計算効果;プログラム検証;トレース意味論;代入;限定継続;ゲーム意味論;shift/reset
      • 無限小プログラミングによるハイブリッドシステムの形式検証手法
        研究活動スタート支援
        京都大学
        末永 幸平
        自 2012年08月31日, 至 2014年03月31日, 採択後辞退
        ハイブリッドシステム;超準解析;型システム;静的検証;形式手法;プログラミング言語;ホーア論理;無限小プログラミング
      • 機械学習技術による高速な演繹的推論エンジンの開発
        基盤研究(B)
        小区分60050:ソフトウェア関連
        千葉大学
        塚田 武志
        自 2022年04月01日, 至 2027年03月31日, 交付
        演繹的推論;機械学習;定理自動証明;システム検証

      外部資金:その他

      • ハイブリッドシステムのための超準プログラミング言語理論を用いた形式手法
        JST さきがけ
        自 2015年10月01日, 至 2019年03月31日
        末永幸平
      • AI集約的サイバーフィジカルシステムの形式的解析手法
        JST CREST
        自 2020年11月01日, 至 2025年03月31日
        末永幸平
      list
        Last Updated :2022/11/23

        教育

        担当科目

        • 自 2022年04月01日, 至 2023年03月31日
          プログラム意味論
          3620, 前期, 情報学研究科, 2
        • 自 2022年04月01日, 至 2023年03月31日
          計算機科学実験及演習2
          9022, 後期, 工学部, 2
        • 自 2022年04月01日, 至 2023年03月31日
          システム検証論
          3666, 後期, 情報学研究科, 2
        • 自 2022年04月01日, 至 2023年03月31日
          計算機科学実験及演習1
          9138, 前期, 工学部, 2
        • 自 2022年04月01日, 至 2023年03月31日
          計算機科学実験及演習3
          9084, 前期, 工学部, 4
        • 自 2022年04月01日, 至 2023年03月31日
          計算機科学実験及演習4
          9039, 後期, 工学部, 3
        • 自 2022年04月01日, 至 2023年03月31日
          プログラミング言語処理系
          9128, 前期, 工学部, 2
        • 自 2013年04月, 至 2014年03月
          計算機科学実験及演習4
          後期, 工学部
        • 自 2014年04月, 至 2015年03月
          計算機科学実験及演習1
          前期, 工学部
        • 自 2014年04月, 至 2015年03月
          計算機科学実験及演習4
          後期, 工学部
        • 自 2014年04月, 至 2015年03月
          コンパイラ
          後期, 工学部
        • 自 2014年04月, 至 2015年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2014年04月, 至 2015年03月
          並列分散システム論
          後期, 情報学研究科
        • 自 2014年04月, 至 2015年03月
          コンピュータ工学特別セミナー
          通年, 情報学研究科
        • 自 2014年04月, 至 2015年03月
          通信情報システム特別研究2
          後期前期, 情報学研究科
        • 自 2014年04月, 至 2015年03月
          通信情報システム特別研究1
          通年, 情報学研究科
        • 自 2015年04月, 至 2016年03月
          Advanced Study in CCE I
          通年, 情報学研究科
        • 自 2015年04月, 至 2016年03月
          Advanced Study in CCE II
          通年, 情報学研究科
        • 自 2015年04月, 至 2016年03月
          コンパイラ
          後期, 工学部
        • 自 2015年04月, 至 2016年03月
          並列分散システム論
          後期, 情報学研究科
        • 自 2015年04月, 至 2016年03月
          ゲーム制作で学ぶ関数型プログラミング言語
          前期, 全学共通科目
        • 自 2015年04月, 至 2016年03月
          コンピュータ工学特別セミナー
          通年, 情報学研究科
        • 自 2015年04月, 至 2016年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2015年04月, 至 2016年03月
          計算機科学実験及演習1
          前期, 工学部
        • 自 2015年04月, 至 2016年03月
          計算機科学実験及演習2
          後期, 工学部
        • 自 2015年04月, 至 2016年03月
          計算機科学実験及演習3
          前期, 工学部
        • 自 2015年04月, 至 2016年03月
          計算機科学実験及演習4
          後期, 工学部
        • 自 2015年04月, 至 2016年03月
          通信情報システム特別研究2
          後期集中, 情報学研究科
        • 自 2015年04月, 至 2016年03月
          通信情報システム特別研究2
          通年, 情報学研究科
        • 自 2015年04月, 至 2016年03月
          通信情報システム特別研究1
          通年, 情報学研究科
        • 自 2016年04月, 至 2017年03月
          Advanced Study in CCE I
          通年, 情報学研究科
        • 自 2016年04月, 至 2017年03月
          Advanced Study in CCE II
          通年, 情報学研究科
        • 自 2016年04月, 至 2017年03月
          ILASセミナー
          前期, 全学共通科目
        • 自 2016年04月, 至 2017年03月
          Parallel and Distributed Systems
          後期, 情報学研究科
        • 自 2016年04月, 至 2017年03月
          コンピュータ工学特別セミナー
          通年, 情報学研究科
        • 自 2016年04月, 至 2017年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2016年04月, 至 2017年03月
          計算機科学実験及演習4
          後期, 工学部
        • 自 2016年04月, 至 2017年03月
          計算機科学のための数学演習
          前期, 工学部
        • 自 2016年04月, 至 2017年03月
          通信情報システム特別研究2
          前期集中, 情報学研究科
        • 自 2016年04月, 至 2017年03月
          通信情報システム特別研究2
          通年, 情報学研究科
        • 自 2016年04月, 至 2017年03月
          通信情報システム特別研究1
          通年, 情報学研究科
        • 自 2017年04月, 至 2018年03月
          Advanced Study in CCE I
          通年, 情報学研究科
        • 自 2017年04月, 至 2018年03月
          Advanced Study in CCE II
          通年, 情報学研究科
        • 自 2017年04月, 至 2018年03月
          Parallel and Distributed Systems
          後期, 情報学研究科
        • 自 2017年04月, 至 2018年03月
          コンピュータ工学特別セミナー
          通年, 情報学研究科
        • 自 2017年04月, 至 2018年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2017年04月, 至 2018年03月
          プログラミング言語処理系
          前期, 工学部
        • 自 2017年04月, 至 2018年03月
          計算機科学実験及演習3
          前期, 工学部
        • 自 2017年04月, 至 2018年03月
          計算機科学のための数学演習
          前期, 工学部
        • 自 2017年04月, 至 2018年03月
          通信情報システム特別研究2
          前期集中, 情報学研究科
        • 自 2017年04月, 至 2018年03月
          通信情報システム特別研究2
          通年, 情報学研究科
        • 自 2017年04月, 至 2018年03月
          通信情報システム特別研究1
          通年, 情報学研究科
        • 自 2018年04月, 至 2019年03月
          Parallel and Distributed Systems
          後期, 情報学研究科
        • 自 2018年04月, 至 2019年03月
          情報と職業
          前期, 工学部
        • 自 2018年04月, 至 2019年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2018年04月, 至 2019年03月
          プログラミング言語処理系
          前期, 工学部
        • 自 2018年04月, 至 2019年03月
          計算機科学実験及演習3
          前期, 工学部
        • 自 2018年04月, 至 2019年03月
          計算機科学のための数学演習
          前期, 工学部
        • 自 2019年04月, 至 2020年03月
          並列分散システム論
          前期, 情報学研究科
        • 自 2019年04月, 至 2020年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2019年04月, 至 2020年03月
          プログラミング言語処理系
          前期, 工学部
        • 自 2019年04月, 至 2020年03月
          計算機科学実験及演習3
          前期, 工学部
        • 自 2019年04月, 至 2020年03月
          計算機科学のための数学演習
          前期, 工学部
        • 自 2020年04月, 至 2021年03月
          並列分散システム論
          後期, 情報学研究科
        • 自 2020年04月, 至 2021年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2020年04月, 至 2021年03月
          プログラミング言語処理系
          前期, 工学部
        • 自 2020年04月, 至 2021年03月
          計算機科学実験及演習3(計算機)
          前期, 工学部
        • 自 2020年04月, 至 2021年03月
          計算機科学のための数学演習
          前期, 工学部
        • 自 2021年04月, 至 2022年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2021年04月, 至 2022年03月
          システム検証論
          後期, 情報学研究科
        • 自 2021年04月, 至 2022年03月
          プログラミング言語処理系
          前期, 工学部
        • 自 2021年04月, 至 2022年03月
          計算機科学実験及演習3(計算機)
          前期, 工学部
        list
          Last Updated :2022/11/23

          大学運営

          部局運営(役職等)

          • 自 2015年04月01日, 至 2017年03月31日
            情報セキュリティ作業委員会委員
          • 自 2015年04月01日, 至 2017年03月31日
            計算機小委員会委員
          • 自 2015年04月01日, 至 2016年03月31日
            ハラスメント窓口相談員
          • 自 2016年04月01日, 至 2017年03月31日
            図書WG委員
          • 自 2017年04月01日, 至 2018年03月31日
            情報セキュリティ作業委員会委員
          • 自 2017年04月01日, 至 2018年03月31日
            計算機小委員会委員
          • 自 2017年04月01日, 至 2018年03月31日
            図書WG委員
          • 自 2018年04月01日, 至 2019年03月31日
            情報セキュリティ委員会委員(情報セキュリティ副技術責任者)
          • 自 2018年04月01日, 至 2019年03月31日
            情報セキュリティ作業委員会委員
          • 自 2018年04月01日, 至 2019年03月31日
            計算機小委員会委員
          • 自 2020年04月01日, 至 2022年03月31日
            図書WG
          • 自 2021年04月01日, 至 2022年03月31日
            連携推進WG委員
          list
            Last Updated :2022/11/23

            学術・社会貢献

            委員歴

            • 自 2019年04月, 至 現在
              運営委員, 日本ソフトウェア科学会プログラミング論研究会
            • 自 2017年04月, 至 2021年05月
              支部委員, 情報処理学会関西支部
            • 自 2013年07月, 至 現在
              専門調査員, 文部科学省科学技術政策研究所科学技術動向研究センター
            • 自 2012年02月, 至 現在
              若手研究者の会, 情報処理学会
            • 自 2019年10月, 至 2020年04月
              5th Workshop on Monitoring and Testing of Cyber-Physical Systems (MT-CPS 2020) プログラム共同委員長
            • 自 2018年03月, 至 2019年03月
              PPL 2019 プログラム共同委員長
            • 自 2015年04月, 至 2019年03月
              運営委員, 情報処理学会プログラミング研究会
            • 自 2015年03月, 至 2017年03月
              幹事, 情報処理学会関西支部
            • FLOPS 2020 プログラム委員
            • PEPM 2018 プログラム委員
            • PPL 2017 プログラム委員
            • APLAS 2015 プログラム委員
            • 実行委員, 第77回情報処理学会大会
            • プログラム委員, ICTAC 2015
            • プログラム委員, HSCC 2015
            • プログラム委員, ACSI 2015
            • 組織委員, PPL 2015
            • 実行委員長, PPL 2014
            • プログラム委員, SACSIS 2013
            • プログラム委員, PEPM 2012
            • MLSE 2020 プログラム委員
            • 自 2021年05月, 至 2022年01月
              POPL 2022 プログラム委員

            学術貢献活動

            • 2022年電子情報通信学会ソサイエティ大会企画セッション「 AI を含むサイバーフィジカルシステムの背景技術 〜信頼性向上を⽬指して〜」
              企画立案・運営等, パネル司会・セッションチェア等
              電子情報通信学会, 自 2022年09月06日, 至 2022年09月06日

            社会貢献活動

            • 巨人の肩の上に立つためのはしごを作るための大工道具
              講師
              宮崎西高等学校, 理文クラス講演会, 自 2021年10月25日
            • PPLサマースクール2019 幹事
              司会, 運営参加・支援
              日本ソフトウェア科学会 プログラミング論研究会, PPLサマースクール2019 「ブロックチェーンと形式検証」, 自 2019年08月26日, 至 2019年08月26日
            • プログラムが正しく動くことを「証明」せよ
              講師
              九州大学マス・フォア・インダストリ研究所・国立研究開発法人科学技術振興機構 (JST), 第29回JST数学キャラバン 拡がりゆく数学 in 福岡, 自 2018年12月15日
            • プログラムが正しく動くことを「証明」せよ
              講師
              岡山大学 数学連携グループ・国立研究開発法人科学技術振興機構 (JST), 広がる数学 IX (第28回 JST 数学キャラバン), 自 2018年11月23日
            • 軽量なプログラム検証のための要素技術
              講師
              国立情報学研究所 オープンハウス2019:産官学連携セミナー 「形式手法・ソフトウェア工学の先端とさらに先:効率的テスト手法と機械学習・人工知能協働」, 自 2019年05月31日
            • 安全性検証技術はビジネスになるか
              講師
              第6回 Entrepreneur Candidate Club(ECC-iCAP) the place where science & entrepreneurship intersect ~科学のフロントランナーが語る未来世界~, 自 2019年05月17日
            • そのプログラム、バグってないですか?:数学を使ってバグを見つけるための形式検証手法
              講師
              2016年度情報処理学会関西支部定期講演会「IoT の周辺技術」, 自 2016年12月21日
            • そのプログラム、バグってないですか? ― 数学を使ってバグを見つける
              講師
              JST 京都大学新技術説明会, 自 2016年05月24日
            • プログラムの「正しさ」の話
              講師
              膳所高校, 自 2015年12月05日
            • Validated Numerics Meets Reachability Analysis for CPS Design (NII Shonan Meeting 2015-14).
              企画
              NII Shonan Meeting, 自 2015年

            ページ上部へ戻る