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

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

京都大学の教員等を検索

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

末永 幸平

スエナガ コウヘイ

情報学研究科 情報学専攻コンピュータ工学講座 准教授

末永 幸平
list
    Last Updated :2025/05/02

    基本情報

    学部兼担

    • 工学部 工学部

    所属学協会

    • 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 :2025/05/02

      研究

      研究テーマ・研究概要

      • 研究テーマ

        形式検証手法

      • 研究概要

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

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

      研究キーワード

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

      研究分野

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

      論文

      • HEIR: A Unified Representation for Cross-Scheme Compilation of Fully Homomorphic Computation.
        Song Bian 0001; Zian Zhao; Zhou Zhang 0016; Ran Mao; Kohei Suenaga; Yier Jin; Zhenyu Guan; Jianwei Liu 0001
        31st Annual Network and Distributed System Security Symposium(NDSS), 2024年09月
      • CHLOE: Loop Transformation over Fully Homomorphic Encryption via Multi-Level Vectorization and Control-Path Reduction.
        Song Bian 0001; Zian Zhao; Ruiyu Shen; Zhou Zhang 0016; Ran Mao; Dawei Li 0009; Yizhong Liu; Masaki Waga; Kohei Suenaga; Zhenyu Guan; Jiafeng Hua; Yier Jin; Jianwei Liu 0001
        IACR Cryptology ePrint Archive, 2024年05月
      • Sharper and Simpler Nonlinear Interpolants for Program Verification.
        Takamasa Okudono; Yuki Nishida 0001; Kensuke Kojima; Kohei Suenaga; Kengo Kido; Ichiro Hasuo
        Programming Languages and Systems - 15th Asian Symposium(APLAS), 2017年
      • Certifying Lyapunov Stability of Black-Box Nonlinear Systems via Counterexample Guided Synthesis
        Chiao Hsieh; Masaki Waga; Kohei Suenaga
        HSCC 2025 (To appear), 2025年05月, 査読有り
      • 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
        ICLR 2025 (To appear), 2025年04月, 査読有り
      • Oblivious Monitoring for Discrete-Time STL via Fully Homomorphic Encryption.
        Masaki Waga; Kotaro Matsuoka; Takashi Suwa; Naoki Matsumoto; Ryotaro Banno; Song Bian 0001; Kohei Suenaga
        Runtime Verification - 24th International Conference(RV), 2024年10月, 査読有り
      • Sharper and Simpler Nonlinear Interpolants for Program Verification.
        Takamasa Okudono; Yuki Nishida; Kensuke Kojima; Kohei Suenaga; Kengo Kido; Ichiro Hasuo
        CoRR, 2017年, 査読有り
      • Hardware Error Detection with In-Situ Monitoring of Control Flow-Related Specifications
        Tomonari Tanaka; Takumi Uezono; Kohei Suenaga; Masanori Hashimoto
        Proceedings of ASP-DAC 2025 (To appear), 2025年01月, 査読有り
      • iCon: Automated Verification of Inter-Transaction Properties in Tezos Smart Contracts with Unknowns
        Yuki Nishida; Kohei Suenaga; Atsushi Igarashi
        2024 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 2024年05月27日, 査読有り
      • StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs.
        Yusuke Kawamoto 0001; Kentaro Kobayashi; Kohei Suenaga
        CoRR, 2024年
      • 命令型プログラムの安全性検証のための所有権主導変換
        小林 亮太; 中村 烈士; 五十嵐 淳; 末永 幸平; 小林 直樹
        PPL 2024 論文集, 2024年03月, 査読有り
      • Sound and Relatively Complete Belief Hoare Logic for Statistical Hypothesis Testing Programs
        Yusuke Kawamoto; Tetsuya Sato; Kohei Suenaga
        Journal of Artificial Intelligence (accepted), 2024年01月, 査読有り, 最終著者
      • Learning Nonlinear Hybrid Automata from Input-Output Time-Series Data.
        Amit Gurung; Masaki Waga; Kohei Suenaga
        ATVA (1), 2023年
      • 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 0005; Erik André Pallas; Akihisa Yamada 0002; Kohei Suenaga; Fuyuki Ishikawa; Kenji Kamijo; Yoshiyuki Shinya; Takamasa Suetomi
        IEEE Transactions on Intelligent Vehicles, 2023年04月
      • HEIR: A Unified Representation for Cross-Scheme Compilation of Fully Homomorphic Computation
        Song Bian; Zian Zhao; Zhou Zhang; Ran Mao; Kohei Suenaga; Yier Jin; Zhenyu Guan; Jianwei Liu
        NDSS'24 (To appear), 2024年, 査読有り
      • Probabilistic Black-Box Checking via Active MDP Learning
        Junya Shijubo; Masaki Waga; Kohei Suenaga
        ACM Transactions on Embedded Computing Systems, 2023年10月31日, 査読有り, 最終著者
      • Formalizing Statistical Causality via Modal Logic
        Yusuke Kawamoto; Tetsuya Sato; Kohei Suenaga
        JELIA 2023, 2023年09月, 査読有り, 最終著者
      • BOREx: Bayesian-Optimization-Based Refinement of Saliency Map for Image- and Video-Classification Models.
        Atsushi Kikuchi; Kotaro Uchida; Masaki Waga; Kohei Suenaga
        ACCV (7), 2022年
      • Feature Attributionを用いたdlshogiの指し手の解釈可能性向上手法
        廣瀬 雄一; 和賀 正樹; 末永 幸平
        研究報告ゲーム情報学（GI）, 2023年03月
      • LLTZ: LLVM IR からスマートコントラクト記述言語 Michelson へのコンパイラ
        臼澤嘉; 末永幸平; 古瀬淳; 五十嵐淳
        第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) 論文集, 2023年03月, 査読有り
      • 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年, 査読有り
        この論文にアクセスする：
      • 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年, 査読有り
      • 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; Shin-ya Katsumata
        Journal of Logical and Algebraic Methods in Programming, 2024年01月, 査読有り
      • スマートコントラクトのための 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年, 査読有り
      • 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年, 査読有り
      • 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年, 査読有り
      • 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

      • Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning
        Minchao Wu; Takeshi Tsukada; Hiroshi Unno; Taro Sekiyama; Kohei Suenaga
        2021年07月16日
      • 昔のネタ帳から
        末永幸平
        コンピュータソフトウェア, 2022年04月, 招待有り
      • PLDI 2016参加報告
        末永 幸平
        コンピュータソフトウェア = Computer software, 2017年02月, 招待有り

      講演・口頭発表等

      • 制御フロー仕様から生成したペトリネットに基づくハードウェア誤動作検出手法
        田中知成; 上薗巧; 末永幸平; 橋本昌宜
        DAシンポジウム 2024, 2024年08月28日
      • Learning nonlinear hybrid automata from input-output time-series data
        Amit Gurung; Masaki Waga; Kohei Suenaga
        ATVA 2023, 2023年10月
      • Probabilistic Black-Box Checking via Active MDP Learning
        Junya Shijubo; Masaki Waga; Kohei Suenaga
        EMSOFT 2023, 2023年09月
      • Formalizing Statistical Causality via Modal Logic
        Yusuke Kawamoto; Tetsuya Sato; Kohei Suenaga
        JELIA 2023, 2023年09月
      • Probabilistic Black-Box Checking via Active MDP Learning
        Junya Shijubo; Masaki Waga; Kohei Suenaga
        EMSOFT 2023, 2023年09月
      • Feature Attributionを用いたdlshogiの指し手の解釈可能性向上手法
        廣瀬 雄一; 和賀 正樹; 末永 幸平
        第49回ゲーム情報学研究発表会, 2023年03月17日
      • SCameleer: スマートコントラクト記述言語SCamlのための自動検証器
        服部佑哉; 西田雄気; 古瀬淳; 末永幸平; 五十嵐淳
        第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 2023年03月08日
      • LLTZ: LLVM IR からスマートコントラクト記述言語 Michelson へのコンパイラ
        臼澤嘉; 末永幸平; 古瀬淳; 五十嵐淳
        第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 2023年03月07日
      • LLTZ: LLVM IR からスマートコントラクト記述言語 Michelson へのコンパイラ
        Yoshi Usuzawa; Kohei Suenaga; Jun Furuse; Atsushi Igarashi
        第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 2023年03月06日
      • Java 検証器 Regnant の帰還
        Ryota Kobayashi; Atsushi Igarashi; Kohei Suenaga
        第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 2023年03月06日
      • 並行命令型プログラミング言語のための所有権篩型システム
        Junya Hirashima; Atsushi Igarashi; Kohei Suenaga
        第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 2023年03月06日
      • ゼロ知識証明を用いて真正性を保証する通信プロトコルのための篩型システム
        Zijian Zhao; Kohei Suenaga; Atsushi Igarashi
        第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023), 2023年03月06日
      • 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日

      書籍等出版物

      • プログラミング言語の形式的意味論入門
        末永 幸平; 勝股 審也; 中澤 巧爾; 西村 進; 前田 敦司, 共訳, G.ウィンスケル
        丸善出版, 2023年01月30日
        京大の蔵書を調べる：
      • 理論計算機科学事典
        徳山, 豪; 小林, 直樹; 岩間, 一雄; 渡辺, 治; 今井, 浩; 南出, 靖彦; 五十嵐, 淳; 長谷川, 真人, 8.3節「型に基づくプログラム検証」
        朝倉書店, 2022年01月
        京大の蔵書を調べる：

      産業財産権

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

      受賞

      • 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日, 交付
        プログラミング言語;プログラム検証;相互運用性;ソフトウェア契約;ソフトウエア契約
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-20H00582/
      • 数学の自動化を推進するための機械学習を用いた定理自動証明手法
        挑戦的研究(萌芽)
        中区分60:情報科学、情報工学およびその関連分野
        京都大学
        末永 幸平
        自 2019年06月28日, 至 2022年03月31日, 完了
        強化学習;自動証明;制約付きホーン節;機械学習;プログラム検証;定理証明;ホーン節ソルバ;人工知能;深層学習
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19K22842/
      • IoT システムのための形式検証手法の深化
        基盤研究(B)
        小区分60050:ソフトウェア関連
        京都大学
        末永 幸平
        自 2019年04月01日, 至 2024年03月31日, 交付
        プログラム検証;形式検証;IoT;モデル検査;PDR;強化学習;機械学習;ハイブリッドシステム;形式手法
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-19H04084/
      • 圏論と数理論理学によるものづくりサポート―ソフトウェア科学のシステム工学への移転
        基盤研究(B)
        国立情報学研究所;東京大学
        蓮尾 一郎
        自 2015年07月10日, 至 2020年03月31日, 完了
        物理情報システム;形式検証;テスト;ハイブリッドシステム;数理論理学;統計的機械学習;圏論;プログラム理論;モデルベース開発;不動点論理;システム工学;応用数学
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15KT0012/
      • 無限小プログラミングによるハイブリッドシステムの形式検証手法
        若手研究(B)
        京都大学
        末永 幸平
        自 2013年04月01日, 至 2016年03月31日, 完了
        ハイブリッドシステム;プログラム検証;不変条件;無限小プログラミング;超準解析;次元解析;非線形不変条件;システム検証;形式手法;形式検証;プログラミング言語;プログラミング言語理論;プログラム意味論;プログラム理論
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25730040/
      • ソフトウェア契約に基づく高階型付プログラムの理論
        基盤研究(B)
        京都大学
        五十嵐 淳
        自 2013年04月01日, 至 2017年03月31日, 完了
        プログラミング言語;ソフトウェア契約;計算効果;プログラム検証;トレース意味論;代入;限定継続;ゲーム意味論;shift/reset
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-25280024/
      • 無限小プログラミングによるハイブリッドシステムの形式検証手法
        研究活動スタート支援
        京都大学
        末永 幸平
        自 2012年08月31日, 至 2014年03月31日, 採択後辞退
        ハイブリッドシステム;超準解析;型システム;静的検証;形式手法;プログラミング言語;ホーア論理;無限小プログラミング
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-24800035/
      • 機械学習技術による高速な演繹的推論エンジンの開発
        基盤研究(B)
        小区分60050:ソフトウェア関連
        千葉大学
        塚田 武志
        自 2022年04月01日, 至 2027年03月31日, 交付
        演繹的推論;機械学習;定理自動証明;CHCソルバ;プログラム検証;システム検証
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-22H03564/
      • 信頼できる統計のための形式検証技術
        基盤研究(B)
        小区分60050:ソフトウェア関連
        国立研究開発法人産業技術総合研究所
        川本 裕輔
        自 2024年04月01日, 至 2027年03月31日, 交付
        形式手法;プログラム検証;統計
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-24K02924/
      • 宇宙線による誤動作の克服に向けた次世代集積システムの信頼性評価基盤技術の開発
        基盤研究(S)
        大区分J
        京都大学
        橋本 昌宜
        自 2024年04月01日, 至 2029年03月31日, 交付
        ソフトエラー;宇宙線;超伝導回路;集積回路;信頼性
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-24H00073/
      • 機械学習技術による高速な演繹的推論エンジンの開発
        基盤研究(B)
        小区分60050:ソフトウェア関連
        千葉大学
        塚田 武志
        自 2022年04月01日, 至 2027年03月31日, 交付
        演繹的推論;機械学習;定理自動証明;プログラム検証;CHCソルバ;システム検証
        https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-23K24820/

      外部資金：その他

      • 輻射を対象とした次世代熱制御材料の研究開発
        国立研究開発法人新エネルギー・産業技術総合開発機構, 官民による若手研究者発掘支援事業／共同研究フェーズ
        自 2021年04月, 至 2026年03月
        坂本雅典
        末永幸平;Daniel Packwood
        研究分担者
      • ハイブリッドシステムのための超準プログラミング言語理論を用いた形式手法
        JST さきがけ
        自 2015年10月01日, 至 2019年03月31日
        末永幸平
      • AI集約的サイバーフィジカルシステムの形式的解析手法
        JST CREST
        自 2020年11月01日, 至 2025年03月31日
        末永幸平
      list
        Last Updated :2025/05/02

        教育

        担当科目

        • 自 2024年04月01日, 至 2025年03月31日
          プログラミング言語処理系
          9128, 前期, 工学部, 2
        • 自 2024年04月01日, 至 2025年03月31日
          システム検証論
          3666, 後期, 情報学研究科, 2
        • 自 2024年04月01日, 至 2025年03月31日
          プログラム意味論
          3620, 前期, 情報学研究科, 2
        • 自 2024年04月01日, 至 2025年03月31日
          計算機科学実験及演習３
          9084, 前期, 工学部, 4
        • 自 2023年04月01日, 至 2024年03月31日
          プログラミング言語処理系
          9128, 前期, 工学部, 2
        • 自 2023年04月01日, 至 2024年03月31日
          システム検証論
          3666, 後期, 情報学研究科, 2
        • 自 2023年04月01日, 至 2024年03月31日
          プログラム意味論
          3620, 前期, 情報学研究科, 2
        • 自 2023年04月01日, 至 2024年03月31日
          計算機科学実験及演習３
          9084, 前期, 工学部, 4
        • 自 2022年04月01日, 至 2023年03月31日
          プログラム意味論
          3620, 前期, 情報学研究科, 2
        • 自 2022年04月01日, 至 2023年03月31日
          計算機科学実験及演習２
          9022, 後期, 工学部, 2
        • 自 2022年04月01日, 至 2023年03月31日
          システム検証論
          3666, 後期, 情報学研究科, 2
        • 自 2022年04月01日, 至 2023年03月31日
          計算機科学実験及演習１
          9138, 前期, 工学部, 2
        • 自 2022年04月01日, 至 2023年03月31日
          計算機科学実験及演習３
          9084, 前期, 工学部, 4
        • 自 2022年04月01日, 至 2023年03月31日
          計算機科学実験及演習４
          9039, 後期, 工学部, 3
        • 自 2022年04月01日, 至 2023年03月31日
          プログラミング言語処理系
          9128, 前期, 工学部, 2
        • 自 2013年04月, 至 2014年03月
          計算機科学実験及演習４
          後期, 工学部
        • 自 2014年04月, 至 2015年03月
          計算機科学実験及演習１
          前期, 工学部
        • 自 2014年04月, 至 2015年03月
          計算機科学実験及演習４
          後期, 工学部
        • 自 2014年04月, 至 2015年03月
          コンパイラ
          後期, 工学部
        • 自 2014年04月, 至 2015年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2014年04月, 至 2015年03月
          並列分散システム論
          後期, 情報学研究科
        • 自 2014年04月, 至 2015年03月
          コンピュータ工学特別セミナー
          通年, 情報学研究科
        • 自 2014年04月, 至 2015年03月
          通信情報システム特別研究２
          後期前期, 情報学研究科
        • 自 2014年04月, 至 2015年03月
          通信情報システム特別研究１
          通年, 情報学研究科
        • 自 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月
          計算機科学実験及演習１
          前期, 工学部
        • 自 2015年04月, 至 2016年03月
          計算機科学実験及演習２
          後期, 工学部
        • 自 2015年04月, 至 2016年03月
          計算機科学実験及演習３
          前期, 工学部
        • 自 2015年04月, 至 2016年03月
          計算機科学実験及演習４
          後期, 工学部
        • 自 2015年04月, 至 2016年03月
          通信情報システム特別研究２
          後期集中, 情報学研究科
        • 自 2015年04月, 至 2016年03月
          通信情報システム特別研究２
          通年, 情報学研究科
        • 自 2015年04月, 至 2016年03月
          通信情報システム特別研究１
          通年, 情報学研究科
        • 自 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月
          計算機科学実験及演習４
          後期, 工学部
        • 自 2016年04月, 至 2017年03月
          計算機科学のための数学演習
          前期, 工学部
        • 自 2016年04月, 至 2017年03月
          通信情報システム特別研究２
          前期集中, 情報学研究科
        • 自 2016年04月, 至 2017年03月
          通信情報システム特別研究２
          通年, 情報学研究科
        • 自 2016年04月, 至 2017年03月
          通信情報システム特別研究１
          通年, 情報学研究科
        • 自 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月
          計算機科学実験及演習３
          前期, 工学部
        • 自 2017年04月, 至 2018年03月
          計算機科学のための数学演習
          前期, 工学部
        • 自 2017年04月, 至 2018年03月
          通信情報システム特別研究２
          前期集中, 情報学研究科
        • 自 2017年04月, 至 2018年03月
          通信情報システム特別研究２
          通年, 情報学研究科
        • 自 2017年04月, 至 2018年03月
          通信情報システム特別研究１
          通年, 情報学研究科
        • 自 2018年04月, 至 2019年03月
          Parallel and Distributed Systems
          後期, 情報学研究科
        • 自 2018年04月, 至 2019年03月
          情報と職業
          前期, 工学部
        • 自 2018年04月, 至 2019年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2018年04月, 至 2019年03月
          プログラミング言語処理系
          前期, 工学部
        • 自 2018年04月, 至 2019年03月
          計算機科学実験及演習３
          前期, 工学部
        • 自 2018年04月, 至 2019年03月
          計算機科学のための数学演習
          前期, 工学部
        • 自 2019年04月, 至 2020年03月
          並列分散システム論
          前期, 情報学研究科
        • 自 2019年04月, 至 2020年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2019年04月, 至 2020年03月
          プログラミング言語処理系
          前期, 工学部
        • 自 2019年04月, 至 2020年03月
          計算機科学実験及演習３
          前期, 工学部
        • 自 2019年04月, 至 2020年03月
          計算機科学のための数学演習
          前期, 工学部
        • 自 2020年04月, 至 2021年03月
          並列分散システム論
          後期, 情報学研究科
        • 自 2020年04月, 至 2021年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2020年04月, 至 2021年03月
          プログラミング言語処理系
          前期, 工学部
        • 自 2020年04月, 至 2021年03月
          計算機科学実験及演習３（計算機）
          前期, 工学部
        • 自 2020年04月, 至 2021年03月
          計算機科学のための数学演習
          前期, 工学部
        • 自 2021年04月, 至 2022年03月
          プログラム意味論
          前期, 情報学研究科
        • 自 2021年04月, 至 2022年03月
          システム検証論
          後期, 情報学研究科
        • 自 2021年04月, 至 2022年03月
          プログラミング言語処理系
          前期, 工学部
        • 自 2021年04月, 至 2022年03月
          計算機科学実験及演習３（計算機）
          前期, 工学部

        指導学生の業績：受賞

        • 第49回GI研究発表会優秀研究賞
          廣瀬雄一, 情報処理学会ゲーム情報学研究会, 2023年05月
        list
          Last Updated :2025/05/02

          大学運営

          部局運営(役職等)

          • 自 2015年04月01日, 至 2017年03月31日
            情報セキュリティ作業委員会委員
          • 自 2015年04月01日, 至 2017年03月31日
            計算機小委員会委員
          • 自 2015年04月01日, 至 2016年03月31日
            ハラスメント窓口相談員
          • 自 2016年04月01日, 至 2017年03月31日
            図書ＷＧ委員
          • 自 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 :2025/05/02

            学術・社会貢献

            委員歴

            • 自 2025年04月
              MLSE 2025 プログラム委員
            • 自 2025年04月
              DSW 2025 プログラム委員
            • プログラム委員長, 第8回機械学習工学研究会（MLSE夏合宿2024）
            • プログラム委員, ATVA 2024
            • 自 2022年10月, 至 2023年09月
              日本ソフトウェア科学会第40回大会プログラム委員長, 日本ソフトウェア科学会
            • 自 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日

            社会貢献活動

            • 研究発表会審査員
              その他
              鹿児島県立加治木高校 総合的な探究の時間(龍門学), 自 2025年01月15日
            • 巨人の肩の上に立つためのはしごを作るための大工道具
              講師
              宮崎西高等学校, 理文クラス講演会, 自 2021年10月25日
            • PPLサマースクール2019 幹事
              司会, 運営参加・支援
              日本ソフトウェア科学会 プログラミング論研究会, PPLサマースクール2019 「ブロックチェーンと形式検証」, 自 2019年08月26日, 至 2019年08月26日
            • プログラムが正しく動くことを「証明」せよ
              講師
              九州大学マス・フォア・インダストリ研究所・国立研究開発法人科学技術振興機構 (JST), 第29回JST数学キャラバン 拡がりゆく数学 in 福岡, 自 2018年12月15日
            • プログラムが正しく動くことを「証明」せよ
              講師
              岡山大学 数学連携グループ・国立研究開発法人科学技術振興機構 (JST), 広がる数学 IX (第２８回 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年

            ページ上部へ戻る