末永幸平(情報学研究科情報学専攻コンピュータ工学講座) | 京都大学教育研究活動データベース

末永幸平

スエナガコウヘイ

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

Last Updated :2025/05/19

基本情報

学部兼担

工学部工学部

所属学協会

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

ORCID ID
0000-0002-7466-8789
J-Global ID
201401093199514640
研究者番号
70633692
外部リンク
https://ksuenaga.github.io/index_ja.html

researchmap URL

https://researchmap.jp/ksuenaga

Last Updated :2025/05/19

研究

研究テーマ・研究概要

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

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

研究キーワード

静的検証

超準解析

形式手法

型システム

ホーア論理

プログラミング言語

無限小プログラミング

ハイブリッドシステム

研究分野

情報通信, ソフトウェア

論文

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; Zian Zhao; Ruiyu Shen; Zhou Zhang; Ran Mao; Dawei Li; Yizhong Liu; Masaki Waga; Kohei Suenaga; Zhenyu Guan; Jiafeng Hua; Yier Jin; Jianwei Liu
Proceedings of 2025 IEEE Symposium on Security and Privacy (SP 2025), 2025年, 査読有り

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 VERiﬁcation (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日
末永幸平

Last Updated :2025/05/19

教育

担当科目

自 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月

Last Updated :2025/05/19

大学運営

部局運営(役職等)

自 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委員

ページ上部へ戻る