略歴
(Ver. 2024/10)
国立情報学研究所 アーキテクチャ科学研究系 教授・数理的高信頼ソフトウェアシステム研究センター長，株式会社イミロン 創業者・取締役，学術博士（Radboud University Nijmegen, 2008）．京都大学数理解析研究所助教，東京大学大学院情報理工学系研究科講師・准教授，国立情報学研究所准教授を経て現職．2016年10月から JST ERATO 蓮尾メタ数理システムデザインプロジェクト研究総括を務める．専門は理論計算機科学，特にシステム検証，プログラミング言語理論，物理情報システム，情報科学における数学的構造に興味を持つ．国際会議 CONCUR 2014, ICECCS 2018, CAV 2023 で論文賞受賞，2024年 科学技術分野の文部科学大臣表彰 科学技術賞受賞．ACM，IEEE, SAE，日本数学会，日本ソフトウェア科学会，情報処理学会，計測自動制御学会，自動車技術会 各会員．
所属学会
ACM, IEEE, SAE, 日本数学会，日本ソフトウェア科学会，情報処理学会，計測自動制御学会，自動車技術会
学歴
職歴
研究費獲得状況
学会活動
- Editorial board member: Journal of Logical and Algebraic Methods in Programming
- Steering committee member:
ATVA,
CMCS,
GaLoP.
- Program
committee
member:
LICS 2016,
CAV 2025,
ASD @ DATE 2025,
ICALP 2025,
TACAS 2025,
Highlights 2024,
RP 2024,
QP 2024,
CAV 2024,
LICS 2024,
CMCS 2024,
FoSSaCS 2024,
ICCPS 2024,
FMAS 2023,
APLAS 2023,
EMSOFT 2023,
ATVA 2023,
CAV 2023,
QP 2023,
FM 2023,
POPL 2023,
EMSOFT 2022,
WADT 2022,
ATVA 2022,
CONCUR 2022,
CMCS 2022,
FASE 2022,
MFPS XXXVII,
QEST 2021,
EMSOFT 2021,
CAV 2021,
FM 2021,
FSCD 2021,
MT-CPS 2021,
POPL 2021,
APLAS 2020,
EMSOFT 2020,
ICFEM 2020,
FMICS 2020,
CONCUR 2020,
NSV 2020,
MT-CPS 2020,
HSCC 2020,
FoSSaCS 2020,
EMSOFT 2019,
CyPhy 2019,
ICFEM 2019,
APLAS 2019,
CALCO 2019,
FORMATS 2019,
CONCUR 2019,
NSV 2019,
ICALP 2019,
FORTE 2019,
SNR 2019,
MT-CPS 2019,
HSCC 2019,
POPL 2019,
CyPhy 2018,
ICFEM 2018,
EMSOFT 2018,
FORMATS 2018,
CONCUR 2018,
CMCS 2018,
LICS 2018,
MT-CPS 2018,
HSCC 2018,
FoSSaCS 2018,
MT-CPS 2017,
LSFA 2017,
CALCO 2017,
HSCC 2017,
QPL 2016,
HSCC 2016,
MT CPS 2016,
CMCS 2016 (chair),
LOLA 2015,
QPL 2015,
CALCO 2015,
LICS 2015,
TTCS 2015,
QPL 2014 (co-chair),
MFPS XXX (2014),
IFIP TCS 2014,
GaLoP 2014,
FLOPS 2014,
ICE 2013,
HAS 2013,
CALCO 2013,
LfSA 2012,
MSFP 2012,
CMCS 2012,
CALCO 2011,
AMAST 2010,
FM-DS 2009,
ICE '09,
ICE '08.
- Organizing committee member:
ATVA 2024 (general chair),
QPL 2014 (chair),
NII Shonan Meeting on Coinduction,
NII Shonan Meeting on Hybrid Systems.
- Member, IFIP WG 1.3 (Foundations of System Specification), from January 2020.
- アドバイザー： 科学技術振興機構（JST） BOOST （若手研究者支援） プログラム（河原林 健一 プログラムオフィサー），2024.8-
- 領域アドバイザー： 科学技術振興機構（JST） ACT-X プログラム，数理・情報のフロンティア 研究領域（河原林 健一 研究総括），2019.4-
- 国内研究会幹事：
SLAGICS 2013,
Adventures of Categories (RIMS WS Ed.) (2011),
ACAN (2011),
Adventures of Categories (2010),
MPP (2008)
著書
雑誌記事など執筆
- 数学通信 第29巻 第3号 (2024年11月) 「数学基礎論の産業応用」，日本数学会．pdf
- 自動車技術 2024年4月号 超の世界 「安全性を数学的証明――自動運転の本格普及へ」，自動車技術会．草稿
- 科学 2023年3月号「自動運転車の安全性の数学的証明――論理学の社会応用の一例として」，岩波書店．pdf
- 計測と制御 2014年12月号「サイバーフィジカルシステムの形式検証――超準解析によるアプローチ」，計測自動制御学会．（末永 幸平氏と共著）．
（以前に書いた草稿をもとにしました）
- 情報処理 2014年7月号「量子プログラミング言語」，情報処理学会．（星野直彦氏と共著）．
（以前に書いた草稿をもとにしました）
- 数理科学 2014年5月号 「計算機科学と代数学――プログラム意味論と普遍代数学」，サイエンス社．
（以前に書いた草稿をもとにしました）
- 数学セミナー連載 「圏論の歩き方」シリーズ構成メンバー (2011年7月号--2012年11月号)，日本評論社．第2回と第6回は記事を執筆．
メディア等
- JSTnews 2024年5月号 特集「自動運転車の安全性の数学的証明に挑戦 公道で通行可能な未来の実現に向けて」
受賞
- 科学技術分野の文部科学大臣表彰 科学技術賞 研究部門，業績名「来るべき情報技術の社会的信頼を担う数理的ソフトウェア研究」 （石川 冬樹氏，勝股 審也氏と共同受賞），2024年4月．
- Distinguished Paper Award (jointly with
Mayuko Kori,
Flavio Ascari,
Filippo Bonchi,
Roberto Bruni,
Roberta Gori), CAV 2023. Certificate
- PPL発表賞（一般の部），第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) （日本ソフトウェア科学会 プログラミング論研究会主催）．
- Outstanding Reviewer Award, EMSOFT 2022.
- Best paper award (jointly with Étienne André and Masaki Waga), ICECCS 2018.
- Best paper award (jointly with Natsuki Urabe), CONCUR 2014.
- 藤原洋数理科学賞 第一回奨励賞，2012年9月．
- PhD (cum laude), Radboud University Nijmegen, 2008.
招待講演他
（他のスライドはこちら）
- Invited talk and tutorial, ICTAC 2024, Bangkok, Thailand, 25 & 27 November 2024.
- 要求仕様と責任範囲の明確化のための論理学的技術： ソフトウェア科学からのアプローチ．
自動車技術会 2024年春季大会 学術講演会 オーガナイズドセッション「自動車制御における産学連携と人材育成」 基調講演．パシフィコ横浜，2024年5月24日．
スライド
- ICT技術への信頼を支える社会インフラとしての数学基礎論と代数学．
日本数学会 2024年度年会 教育研究資金問題検討委員会シンポジウム 「数学と諸分野の連携が創出する数学研究」 講演．大阪公立大学 杉本キャンパス，2024年3月19日．
スライド
- 総合信頼性の数学．
情報処理学会 第86回全国大会 「完全無欠な情報システムはあり得るのか？ ～リスクと総合信頼性～」セッション 特別講演．
神奈川大学 横浜キャンパス，2024年3月16日．
スライド
- Invited talk, the 3rd Workshop on Safety Testing and Validation of Connected and Automated Vehicles at ITSC 2023, Bilbao, Spain, 24 September 2023.
- Panelist, Verification Mentoring Workshop at CAV 2023. 18 July 2023.
-
ICT技術の信頼を支える社会インフラとしてのソフトウェア科学．
情報学科・専攻協議会，
2023年07月15日．オンライン．
スライド
- OASIS: The Oxford Advanced Seminar on Informatic Structures, 19,
20,
21,
June 2023.
-
Breaking Through Two Walls: from Categorical Metatheory to Formal Verification of Safety of Automated Driving. 第25回プログラミングおよびプログラミング言語ワークショップ (PPL 2023) （日本ソフトウェア科学会 プログラミング論研究会主催）．名古屋大学，2023年3月8日．PPL発表賞受賞（一般の部）．
スライド
-
自動運転車の安全性の数学的証明： ICT新技術の社会受容のための数学と論理学．NII 記者懇談会，オンライン，2023年2月22日．スライド
-
CASE安全性の論理的保証： 最先端ソフトウェア研究の成果から．SDVフォーラム 車載ソフトウェアDay，第16回 オートモーティブワールド，東京ビッグサイト，2023年1月24日．
-
ソフトウェア理論研究のシステムディペンダビリティ応用： 圏論的基礎理論から自動運転安全性証明まで．第20回ディペンダブルシステムワークショップ，日本ソフトウェア科学会 ディペンダブルシステム研究会，日本大学駿河台キャンパス，2022年12月15日．
スライド
-
数学的証明の社会・産業応用．九州大学マス・フォア・イノベーション連係学府 設置記念シンポジウム，九州大学，2022年6月28日．スライド
-
Blackbox Analysis of Automotive Systems by Logic and Optimization
Software Science Approaches to Efficiency and Deployability.
自動車技術会 2022年春季大会 学術講演会 オーガナイズドセッション「自動車制御とモデリング -新しい課題と新しいアプローチ-」．パシフィコ横浜，2022年5月27日．
スライド
-
自動車システムの安全性保証へのソフトウェア科学的アプローチ――論理的アカウンタビリティと適用コスト軽減の両立．第7回
オートモーティブ・ソフトウェア・フロンティア （主催： 株式会社インプレス，共催： 名古屋大学 未来社会創造機構 モビリティ社会研究所），オンライン．2022年2月25日．
スライド
-
数学的証明の社会・産業応用――ICTシステムの信頼性保証と，Science of Sciences としての社会貢献．シンポジウム「社会課題は数理科学で解決できる！？ －試みと課題－」，名古屋大学 野依記念学術交流館 ＆ オンライン，
2021年10月26日．
スライド
-
数学的証明の社会・産業応用――ICTシステムの信頼性保証と，Science of Sciences としての社会貢献．
経団連
数理活用産学連携イニシアティブ 第1回．オンライン開催，2021年7月16日．
- Programming Languages Mentoring Workshop (PLMW) @ POPL 2021 (online).
18 January 2021.
- 量子プログラミング言語の研究：静的解析から量子プログラム統合開発環境へ．
情報処理学会 連続セミナー 2020 第６回「量子コンピュータとソフトウェア」．オンライン開催，2020年12月14日．
スライド
- サイバーフィジカルシステムの安全性保証――統計的機械学習の不確かさに対処するソフトウェア科学・工学的手法．
自動車技術会 自動車制御とモデル研究部門委員会 公開委員会「サイバーフィジカルシステムと人間社会・AI」，上智大学四谷キャンパス，2020年1月30日．
スライド
- 理論計算機科学入門 有限と無限のあいだ
－数学的理論から、AI・自動運転－．国立情報学研究所 市民講座「情報学最前線」，2019年11月7日．
ビデオ
スライド
-
日本機械学会関西支部 2019年度 特別フォーラム
～ Society5.0がめざす新しい社会 ～，大阪科学技術センター，2019年9月20日．
スライド
-
Coalgebra, Now @ FLoC 2018 Workshop, Oxford, UK.
8 July 2018.
-
Game Semantics 25 Workshop, Oxford, UK.
8 July 2018.
-
物理情報システムの検証手法：制御と形式手法の相互理解，そして協働へ．
第61回自動制御連合講演会．南山大学，2018年11月17日．
スライド
- 統計的機械学習と演繹的形式推論: システムの信頼性と説明可能性へのアプローチ．数学連携ワークショップ
Society 5.0と数学 2
---人工知能研究と数学とのかかわり---．岡山大学，2018年9月24日．スライド
- SynCoP 2018,
Thessaloniki, Greece.
15 April 2018.
- CyPhy 2017,
Seoul, South Korea.
19 October 2017.
- 日本ソフトウェア科学会第34回大会 若手特別講演．横浜市，2017年9月21日．
- FSCD 2016, Porto, Portugal, June 24, 2016.
- はたらく現代抽象数学： 理論計算機科学からの視点，名古屋大学大学院多元数理科学研究科 談話会，名古屋大学，2015年11月25日．
- 超準解析による物理情報システムの形式検証―離散から連続・ ハイブリッドへ，大阪大学 数理・データ科学セミナー 数理モデルセミナーシリーズ 第2回，大阪大学 豊中キャンパス 基礎工国際棟シグマホール，2015年6月12日．
- CMCS 2014, Grenoble, France, April 2014.
- 超準解析による物理情報システムの形式検証------離散から連続・
ハイブリッドへ．企画特別講演，日本数学会 秋季総合分科会，愛媛大学，2013年9月．
- GaLoP VIII, Queen Mary Univ. London. July 2013.
- ICE 2012,
5th Workshop on Interaction and Concurrency Experience,
Stockholm, June 16, 2012,
a satelite event of DisCoTec 2012.
講義ノート
集中講義
- Introduction to Algebra and Coalgebra, 名古屋大学 多元数理科学研究科. 2013年7月.
- Introduction to Categorical Algebra and Coalgebra，京都大学 数理解析研究所． 2012年7-8月.
雑文
生い立ち
- 1978年9月，福岡県大牟田市生まれ．小宮塾 31期，ラ・サール高校卒．
- 男性，既婚，息子一人．