山本光晴 (Mitsuharu Yamamoto) - マイポータル

基本情報

所属: 千葉大学大学院理学研究院数学・情報数理学研究部門情報数理講座教授

学位: 博士(理学)(東京大学)

J-GLOBAL ID: 200901038903211330
researchmap会員ID: 1000222032

研究分野

情報通信 / 情報学基礎論 /

経歴

2017年6月 - 現在

千葉大学, 大学院理学研究院数学・情報数理学研究部門, 教授
2017年4月 - 2017年5月

千葉大学, 大学院理学研究院数学・情報数理学研究部門, 准教授
2007年4月 - 2017年3月

千葉大学, 大学院理学研究科基盤理学専攻数学・情報数理学コース, 准教授
2003年8月 - 2007年3月

千葉大学, 理学部数学・情報数理学科, 助教授
1996年10月 - 2003年7月

千葉大学, 理学部数学・情報数理学科, 助手

学歴

1996年4月 - 1996年10月

東京大学, 大学院理学系研究科, 情報科学専攻博士課程(中退)
1994年4月 - 1996年3月

東京大学, 大学院理学系研究科, 情報科学専攻修士課程
1992年4月 - 1994年3月

東京大学, 理学部, 情報科学科
1990年4月 - 1992年3月

東京大学, 教養学部, 理科I類

論文

Model‐based testing of Apache ZooKeeper: Fundamental API usage and watchers

Cyrille Artho, Kazuaki Banzai, Quentin Gros, Guillaume Rousset, Lei Ma, Takashi Kitamura, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto

Software Testing, Verification and Reliability 30(7-8) 2020年11月査読有り
Model-based API Testing of Apache ZooKeeper

Cyrille Artho, Quentin Gros, Guillaume Rousset, Kazuaki Banzai, Lei Ma, Takashi Kitamura, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto

2017 10TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST) 288-298 2017年査読有り
Formalization of Karp-Miller Tree Construction on Petri Nets

Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto

PROCEEDINGS OF THE 6TH ACM SIGPLAN CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP'17 66-78 2017年査読有り
Automated Dataset Construction from Web Resources with Tool Kayur

Alexander Kohan, Mitsuharu Yamamoto, Cyrille Artho

2016 FOURTH INTERNATIONAL SYMPOSIUM ON COMPUTING AND NETWORKING (CANDAR) 7(2) 98-104 2016年査読有り
Java Pathfinder on Android Devices

Alexander Kohan, Mitsuharu Yamamoto, Cyrille Artho, Yoriyuki Yamagata, Lei Ma, Masami Hagiya, Yoshinori Tanabe

ACM SIGSOFT Software Engineering Notes 41(6) 1-5 2016年査読有り
Formalization of Bing's Shrinking Method in Geometric Topology

Ken'ichi Kuga, Manabu Hagiwara, Mitsuharu Yamamoto

Intelligent Computer Mathematics 9791 18-27 2016年査読有り
Runtime Monitoring for Concurrent Systems

Yoriyuki Yamagata, Cyrille Artho, Masami Hagiya, Jun Inoue, Lei Ma, Yoshinori Tanabe, Mitsuharu Yamamoto

RUNTIME VERIFICATION, (RV 2016) 10012 386-403 2016年査読有り
Automated Dataset Construction from Web Resources with Tool Kayur

Alexander Kohan, Mitsuharu Yamamoto, Cyrille Artho

2016 FOURTH INTERNATIONAL SYMPOSIUM ON COMPUTING AND NETWORKING (CANDAR) 98-104 2016年査読有り
GRT at the SBST 2015 Tool Competition

Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto

2015 IEEE/ACM 8TH INTERNATIONAL WORKSHOP ON SEARCH-BASED SOFTWARE TESTING (SBST) 48-51 2015年査読有り
Software Model Checking of UDP-based Distributed Applications

Nazim Sebih, Masami Hagiya, Franz Weitl, Mitsuharu Yamamoto, Cyrille Artho, Yoshinori Tanabe

International Journal of Networking and Computing 5(2) 373-402 2015年査読有り
Cardinality of UDP Transmission Outcomes

Franz Weitl, Nazim Sebih, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Mitsuharu Yamamoto

DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, SETTA 2015 9409 120-134 2015年査読有り
Modular Software Model Checking for Distributed Systems

Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto, Koichi Takahashi

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 40(5) 483-501 2014年5月査読有り
Using Checkpointing and Virtualization for Fault Injection

Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Eric Platon, Richard Potter, Kuniyasu Suzaki, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto

2014 SECOND INTERNATIONAL SYMPOSIUM ON COMPUTING AND NETWORKING (CANDAR) 5(2) 144-150 2014年査読有り
Software Model Checking of UDP-based Distributed Applications

Nazim Sebih, Franz Weitl, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto

2014 SECOND INTERNATIONAL SYMPOSIUM ON COMPUTING AND NETWORKING (CANDAR) 96-105 2014年査読有り
Using Checkpointing and Virtualization for Fault Injection

Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Eric Platon, Richard Potter, Kuniyasu Suzaki, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto

2014 SECOND INTERNATIONAL SYMPOSIUM ON COMPUTING AND NETWORKING (CANDAR) 144-150 2014年査読有り
可変長情報源符号化逆定理の形式化

小尾良介, 萩原学, 山本光晴

第37回情報理論とその応用シンポジウム 494-499 2014年
Software model checking for distributed systems with selector-based, non-blocking communication

Cyrille Artho, Masami Hagiya, Richard Potter, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto

2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013 - Proceedings 169-179 2013年査読有り
Modbat: A model-based API tester for event-driven systems

Cyrille Valentin Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, Mitsuharu Yamamoto

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 8244 112-128 2013年査読有り
Coqに於いてモナドを用いたプログラム記述と推論を行う為の統合環境の構築に向けて

須田啓司, 山本光晴

日本ソフトウェア科学会第29回大会萌芽セッション 2012年
Model checking distributed systems by combining caching and process checkpointing

Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto

2011 26th IEEE/ACM International Conference on Automated Software Engineering, ASE 2011, Proceedings 103-112 2011年査読有り

もっとみる

MISC

グラフ探索アルゴリズムの形式的検証とモデル検査への応用について (プログラム変換と記号・数式処理)

山本光晴, 高橋孝一, 萩谷昌己, 西崎真也, 玉井哲雄

数理解析研究所講究録 1125 129-141 2000年1月

書籍等出版物

化学系・生物系の計算モデル

萩谷昌己, 山本光晴 (担当:共著, 範囲:全6章のうち、第2章・第6章の全てと、第4章の一部を担当)

共立出版 2009年 (ISBN: 9784320121829)

講演・口頭発表等

ペトリネットにおける到達可能性問題の変種間の還元可能性の形式化

手塚凜, 山本光晴

第20回定理証明及び定理証明系ミーティング(TPP2024) 2024年11月26日
VASSからVASへの変換の形式化

脇坂勝大, 山本光晴

第19回定理証明及び定理証明系ミーティング(TPP2023) 2023年10月31日
VASSからVASへの変換のMathCompによる形式化

脇坂勝大, 山本光晴

日本ソフトウェア科学会第40回大会 2023年9月13日
ペトリネットにおける停止性判定の形式化

稲垣衛, 山本光晴

第15回定理証明及び定理証明系ミーティング(TPP2019) 2019年11月19日
ペトリネットにおける有界性に関する性質のCoq/SSReflectによる形式化

稲垣衛, 山本光晴

第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019) ポスターセッション 2019年3月7日
ニューラルネットワークにおける表現可能なデータ数のSSReflectによる形式化

井上健太, 山本光晴

第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019) ポスターセッション 2019年3月7日
ペトリネットにおける有界性判定の形式化

稲垣衛, 山本光晴

第14回定理証明及び定理証明系ミーティング(TPP2018) 2018年11月21日
Formalization of Karp-Miller Tree Construction on Petri Nets

山本光晴, 関根祥吾, 松本早貴

第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017) カテゴリ2 2017年3月9日
ペトリネットにおけるKarp-Miller木構成と被覆性判定の正当性の形式化

松本早貴, 山本光晴

第12回定理証明及び定理証明系ミーティング(TPP2016) 2016年11月15日
Acquisition and Preprocessing of Bug Reports from Multiple Data Sources with Tool Kayur

Alexander Kohan, Cyrille Artho, Mitsuharu Yamamoto

23rd IEEE International Conference on Software Analysis, Evolution, and Reengineering (SANER2016) Poster Session 2016年3月15日
A formal proof of Higman's lemma in Coq/Ssreflect

山本光晴

第11回定理証明及び定理証明系ミーティング(TPP2015) 2015年9月17日
ペトリネットに対するKarp-Miller木構成のCoq/Ssreflectによる実装

松本早貴, 山本光晴

第11回定理証明及び定理証明系ミーティング(TPP2015) 2015年9月17日
定理証明系Coqを用いたSibling Propertyとハフマン木との同値性の形式的証明

須田啓司, 山本光晴

第14回プログラミングおよびプログラミング言語ワークショップ(PPL2012) ポスターセッション 2012年3月9日

所属学協会

Works(作品等)

Emacs Mac port (distributed as a separate patch set based on GNU Emacs 23-29)

山本光晴

2009年8月 - 現在コンピュータソフト
Emacs Carbon+AppKit port (distributed as a separate patch set based on GNU Emacs 22.3)

山本光晴

2008年9月コンピュータソフト
Emacs Carbon port (included in the standard distribution of GNU Emacs 22)

Free Software Foundation, Inc

2007年6月コンピュータソフト

共同研究・競争的資金等の研究課題

ベクトル加算系における到達可能性問題の決定可能性の形式化

日本学術振興会科学研究費助成事業基盤研究(C) 2018年4月 - 2023年3月

山本光晴
ソフトウェアモデル検査における活性検証

日本学術振興会科学研究費助成事業基盤研究(C) 2016年4月 - 2019年3月

田辺良則, 山本光晴, 萩谷昌己
4次元ポアンカレ予想を含む幾何的トポロジーの形式化

日本学術振興会科学研究費助成事業挑戦的萌芽研究 2015年4月 - 2018年3月

久我健一, 萩原学, 山本光晴
実行時検証とモデル検査の融合によるネットワークソフトウェアの統合実行監視

日本学術振興会科学研究費助成事業基盤研究(B) 2014年4月 - 2017年3月

山本光晴, 萩谷昌己, Artho Cyrille, 山形頼之, 田辺良則, コハンアレクサンダー, ヴァイテルフランツ, 馬雷, セビナジム
定理証明器によるモジュラーなソフトウェア検証

日本学術振興会科学研究費助成事業基盤研究(C) 2013年4月 - 2016年3月

田辺良則, 萩谷昌己, 山本光晴, 湯浅能史, 逸見港
クラウドコンピューティングミドルウェアのソフトウェアモデル検査手法

日本学術振興会科学研究費助成事業基盤研究(A) 2011年4月 - 2016年3月

萩谷昌己, アルトシリル, 山本光晴, 田辺良則, 横山重俊, ヴァイテルフランツ, ポッターリチャード, レオンワタナキットワチャリン
分散チェックポインティングを用いたネットワークアプリケーションのモデル検査

日本学術振興会科学研究費助成事業基盤研究(B) 2011年4月 - 2014年3月

山本光晴, 萩谷昌己, アルトシリル, 田辺良則, レオンワタナキットワチャリン, ヴァイテルフランツ, ポッターリチャード, セビナジム
仮想計算機によるコミュニケーションバックトラッキングとモデル検査への応用

日本学術振興会科学研究費助成事業基盤研究(B) 2008年 - 2010年

山本光晴, 萩谷昌己, アルトシリル, 田辺良則, 高橋孝一
チャーチのラムダ計算のBCK論理による再生

日本学術振興会科学研究費助成事業基盤研究(C) 2003年 - 2006年

古森雄一, 櫻井貴文, 山本光晴, 廣川左千男, 藤田憲悦, 鹿島亮, 多田充
抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証

日本学術振興会科学研究費助成事業特定領域研究 2004年 - 2005年

山本光晴, 萩谷昌己, 辻尚史
スタイン現象および縮小推定法の新展開

日本学術振興会科学研究費助成事業基盤研究(C) 2001年 - 2004年

今野良彦, 白石高章, 滝澤由美, 中神祥臣, 峰村勝弘, 中神潤一, 安田正実, 田栗正章, 山本光晴
抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証

日本学術振興会科学研究費助成事業特定領域研究 2003年 - 2003年

山本光晴, 高橋孝一, 辻尚史, 萩谷昌己
抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証

日本学術振興会科学研究費助成事業特定領域研究 2002年 - 2002年

山本光晴, 高橋孝一, 辻尚史, 萩谷昌己
抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証

日本学術振興会科学研究費助成事業特定領域研究(C) 2001年 - 2001年

山本光晴, 萩谷昌己
論理体系の意味論と文法的性質の関係

日本学術振興会科学研究費助成事業基盤研究(C) 2000年 - 2001年

桜井貴文, 山本光晴, 古森雄一, 辻尚史
描象モデル検査とその応用

日本学術振興会科学研究費助成事業基盤研究(B) 1999年 - 2001年

萩谷昌己, 山本光晴, 高橋孝一, 玉井哲雄
状態空間モデルに基づく縦断的データの解析へのブートストラップ法による接近

日本学術振興会科学研究費助成事業基盤研究(B) 1998年 - 2000年

田栗正章, 今野良彦, 種村秀紀, 中神潤一, 橋本明浩, 宮埜壽夫, 桜井貴文, 古森雄一, 渚勝, 中村吉邑, 山本光晴
型理論の意味論と文法的性質の関係

日本学術振興会科学研究費助成事業基盤研究(C) 1998年 - 1999年

桜井貴文, 山本光晴, 古森雄一, 辻尚史, 西崎真也, 腰越秀之
部分構造論理の研究

日本学術振興会科学研究費助成事業基盤研究(C) 1998年 - 1999年

古森雄一, 金沢誠, 山本光晴, 桜井貴文, 藤田憲悦, 廣川佐千男

山本光晴

基本情報

研究分野

経歴

学歴

論文

MISC

書籍等出版物

講演・口頭発表等

所属学協会

Works(作品等)

共同研究・競争的資金等の研究課題

メニュー

共著者の一覧