Yamamoto Mitsuharu 山本光晴

… Alternative Names

YAMAMOTO Mitsuharu 山本光晴

Less

Researcher Number	00291295
Other IDs
Affiliation (Current)	2025: 千葉大学, 大学院理学研究院, 教授
Affiliation (based on the past Project Information) *help	2017 – 2023: 千葉大学, 大学院理学研究院, 教授 2014 – 2016: 千葉大学, 大学院理学研究科, 准教授 2011 – 2016: 千葉大学, 理学(系)研究科(研究院), 准教授 2008 – 2011: Chiba University, 大学院・理学研究科, 准教授 2003 – 2006: 千葉大学, 理学部, 助教授 1998 – 2002: 千葉大学, 理学部, 助手
Review Section/Research Field	Principal Investigator Science and Engineering / Software / Basic Section 60010:Theory of informatics-related / Software Except Principal Investigator 計算機科学 / Statistical science / Software / General mathematics (including Probability theory/Statistical mathematics) / General mathematics (including Probability theory/Statistical mathematics) / Software
Keywords	Principal Investigator 証明検証系 / 形式的手法 / グラフ書き換え / 抽象モデル検査 / モデル検査 / チェックポインティング / セルオートマトン / 時相論理 / 時間ペトリネット / 時間付きオートマトン … More / 時間付き多重集合書き換え / ペトリネット / 到達可能性 / ベクトル加算系 / 形式化 / 定理証明支援系 / ネットワークソフトウェア / 実行時検証 / 実環境モデル検査 / 仮想計算機 / グラフ探索 … More Except Principal Investigator 部分構造論理 / model checking / モデル検査 / 文法的性質 / Type Theory / Lambda Calculus / BCK Logic / Intuitionistic Logic / Classical Logic / Substructural Logic / 型理論 / ラムダ計算 / BCK論理 / 直観主義論理 / 古典論理 / ソフトウェア検証 / 仕様記述・検証 / ソフトウエア学 / アルゴリズム / ソフトウェア / Java / liveness / software / Illative Combinatory Logic / Russel's Paradox / Curry-Howard isomorphism / Church / 極小論理式 / P=NP問題 / 数理論理学 / 集合論 / ラッセルの逆理 / Curry-Howard対応 / チャーチ / growth curve / simultaneous estimation / covariance matrix / two-sample problems / improved estimators / 同時推定 / グラフィカルモデル / 縮小推定 / スタイン推定量 / 成長曲線モデル / 同時推定問題 / 共分散行列 / 2標本問題 / 改良型推定量 / α-conversion / substitution / first-class context / explicit substitution / cut elimination / intuitionistic modal logic / modal substructural logic / context / explicit environment / 正規化 / α変換 / 束縛変数 / 代入操作 / 文脈 / 明示的代入 / カット除去 / 直観主義的様相論理 / 様相部分構造命題論理 / security / concurrent garbage / graph search / theorem proving / abstract interpretation / Verification / 並行ゴミ集め / セキュリティ / 並列ゴミ集め / グラフ探索 / 定理証明 / 抽象解釈 / 検証 / Strong Normalization / Syntactic Property / Category Theory / Model / Semantics / 部分構造理論 / 強正規化 / 強制規化 / カテゴリ理論 / モデル / 意味論 / Simulation / Size and power of tests / Area difference statistic / AR model / Moving block / Bootstrap test / Test of curve difference / Wind velocity data by artificial satellite / AUC-統計量 / ordered moving block bootstrap法 / カルマンフィルター / longitudinal data / 人工衛星データ / 検出力のシミュレーション / 2種類の曲線の差の検定 / moving block bootstrap法 / 状態空間モデル / ブートストラップ検定 / シミュレーション / 検定のサイズ・検出力 / 面積差統計量 / ARモデル / moving block / bootstrap検定 / 曲線の差の検定 / 人工衛星風速データ / コード抽出 / 型推論 / Coq / ディペンダブル・コンピューティング / 定理証明支援系 / クラウドコンピューティング / ソフトウェアモデル検査 / 仕様記述・仕様検証 Less

Formalization of the decidability of the reachability problem for vector addition systemsPrincipal Investigator
- Principal Investigator
  
  Yamamoto Mitsuharu
- Project Period (FY)
  2018 – 2023
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Chiba University
Liveness verification in software model checking
- Principal Investigator
  
  Tanabe Yoshinori
- Project Period (FY)
  2016 – 2018
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Software
- Research Institution
  Tsurumi University
Integrated Runtime Monitoring of Network Software by Fusion of Runtime Verification and Model CheckingPrincipal Investigator
- Principal Investigator
  
  Yamamoto Mitsuharu
- Project Period (FY)
  2014 – 2016
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Chiba University
Modular software verification with a proof assistant
- Principal Investigator
  
  TANABE Yoshinori
- Project Period (FY)
  2013 – 2015
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Software
- Research Institution
  Tsurumi University
  National Institute of Informatics
Software model checking methods for cloud computing middleware
- Principal Investigator
  
  Hagiya Masami
- Project Period (FY)
  2011 – 2015
- Research Category
  
  Grant-in-Aid for Scientific Research (A)
- Research Field
  
  Software
- Research Institution
  The University of Tokyo
Model Checking Network Applications using Distributed CheckpointingPrincipal Investigator
- Principal Investigator
  
  YAMAMOTO Mitsuharu
- Project Period (FY)
  2011 – 2013
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Chiba University
Communication Backtracking by Virtual Machines and Applications to Model CheckingPrincipal Investigator
- Principal Investigator
  
  YAMAMOTO Mitsuharu
- Project Period (FY)
  2008 – 2010
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Software
- Research Institution
  Chiba University
抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証Principal Investigator
- Principal Investigator
  
  山本光晴
- Project Period (FY)
  2004 – 2005
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  Chiba University
抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証Principal Investigator
- Principal Investigator
  
  山本光晴
- Project Period (FY)
  2003
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  Chiba University
Regeneration of Church's Lambda calculus on BCK logic
- Principal Investigator
  
  KOMORI Yuichi
- Project Period (FY)
  2003 – 2006
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  General mathematics (including Probability theory/Statistical mathematics)
- Research Institution
  Chiba University
抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証Principal Investigator
- Principal Investigator
  
  山本光晴
- Project Period (FY)
  2002
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas
- Review Section
  
  Science and Engineering
- Research Institution
  Chiba University
抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証Principal Investigator
- Principal Investigator
  
  山本光晴
- Project Period (FY)
  2001
- Research Category
  
  Grant-in-Aid for Scientific Research on Priority Areas (C)
- Review Section
  
  Science and Engineering
- Research Institution
  Chiba University
Stein phenomena and further development on shrinkage methods
- Principal Investigator
  
  KONNO Yoshihiko
- Project Period (FY)
  2001 – 2004
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Statistical science
- Research Institution
  Japan Women's University
  Chiba University
Relation between Semantics of Logical System and its Syntactic Properties
- Principal Investigator
  
  SAKURAI Takafumi
- Project Period (FY)
  2000 – 2001
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  計算機科学
- Research Institution
  CHIBA UNIVERSITY
Abstract Model Cheking and Its Applications
- Principal Investigator
  
  HAGIYA Masami
- Project Period (FY)
  1999 – 2001
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  計算機科学
- Research Institution
  The University of Tokyo
State-space model approach to longitudinal data analysis by bootstrap
- Principal Investigator
  
  TAGURI Masaaki
- Project Period (FY)
  1998 – 2000
- Research Category
  
  Grant-in-Aid for Scientific Research (B).
- Research Field
  
  Statistical science
- Research Institution
  Chiba University
A Study of Substractural Logics
- Principal Investigator
  
  KOMORI Yuichi
- Project Period (FY)
  1998 – 1999
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  General mathematics (including Probability theory/Statistical mathematics)
- Research Institution
  Chiba University
Relation between Semantics of Type Theory and its Syntactic Properties
- Principal Investigator
  
  SAKURAI Takafumi
- Project Period (FY)
  1998 – 1999
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  計算機科学
- Research Institution
  Chiba University

[Journal Article] Model-based API Testing of Apache ZooKeeper2017
- Author(s)
  Cyrille Valentin Artho, Quentin Gros, Guillaume Rousset, Kazuaki Banzai, Lei Ma, Takashi Kitamura, Masami Hagiya, Yoshinori Tanabe, and Mitsuharu Yamamoto
- Journal Title
  
  10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)
  
  Volume: 印刷中
- Peer Reviewed / Acknowledgement Compliant / Open Access
- Data Source
  KAKENHI-PROJECT-26280019
[Journal Article] Formalization of Karp-Miller tree construction on petri nets2017
- Author(s)
  Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto
- Journal Title
  
  Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
  
  Volume: － Pages: 66-78
- DOI
  10.1145/3018610.3018626
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-16K00109
[Journal Article] Runtime Monitoring for Concurrent Systems2016
- Author(s)
  Yoriyuki Yamagata, Cyrille Artho, Masami Hagiya, Jun Inoue, Lei Ma, Yoshinori Tanabe, and Mitsuharu Yamamoto
- Journal Title
  
  Runtime Verification - 16th International Conference, (RV 2016)
  
  Volume: LNCS 10012 Pages: 386-403
- DOI
  10.1007/978-3-319-46982-9_24
- ISBN
  9783319469812, 9783319469829
- Peer Reviewed / Acknowledgement Compliant / Open Access
- Data Source
  KAKENHI-PROJECT-26280019
[Journal Article] Java Pathfinder on Android Devices2016
- Author(s)
  Alexander Kohan, Mitsuharu Yamamoto, Cyrille Artho, Yoriyuki Yamagata, Lei Ma, Masami Hagiya, and Yoshinori Tanabe
- Journal Title
  
  ACM SIGSOFT Software Engineering Notes
  
  Volume: 41(6) Issue: 6 Pages: 1-5
- DOI
  10.1145/3011286.3011292
- Peer Reviewed / Acknowledgement Compliant / Open Access
- Data Source
  KAKENHI-PROJECT-26280019
[Journal Article] Software Model Checking of UDP-based Distributed Applications2015
- Author(s)
  Nazim Sebih, Masami Hagiya, Franz Weitl, Mitsuharu Yamamoto, Cyrille Artho, Yoshinori Tanabe
- Journal Title
  
  International Journal of Networking and Computing
  
  Volume: 5 Issue: 2 Pages: 373-402
- DOI
  10.15803/ijnc.5.2_373
- NAID
  130005091737
- ISSN
  2185-2839, 2185-2847
- Language
  English
- Peer Reviewed / Acknowledgement Compliant / Open Access
- Data Source
  KAKENHI-PROJECT-26280019
[Journal Article] GRT at the SBST 2015 Tool Competition2015
- Author(s)
  Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
- Journal Title
  
  Proc 8th IEEE/ACM International Workshop on Search-Based Software Testing
  
  Volume: 2015 Pages: 48-51
- DOI
  10.1109/sbst.2015.19
- Peer Reviewed / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
[Journal Article] Cardinality of UDP Transmission Outcomes2015
- Author(s)
  Franz Weitl, Nazim Sebih, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Mitsuharu Yamamoto
- Journal Title
  
  Proc 1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications
  
  Volume: 2015 Pages: 120-134
- DOI
  10.1007/978-3-319-25942-0_8
- ISBN
  9783319259413, 9783319259420
- Peer Reviewed / Acknowledgement Compliant / Open Access
- Data Source
  KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
[Journal Article] Software Model Checking of UDP-based Distributed Applications2015
- Author(s)
  Nazim Sebih, Masami Hagiya, Franz Weitl, Mitsuharu Yamamoto, Cyrille Artho, Yoshinori Tanabe
- Journal Title
  
  International Journal of Networking and Computing
  
  Volume: 5 Pages: 373-402
- NAID
  130005091737
- Peer Reviewed / Acknowledgement Compliant / Open Access
- Data Source
  KAKENHI-PROJECT-23240003
[Journal Article] Using Checkpointing and Virtualization for Fault Injection2015
- Author(s)
  Cyrille Artho, Kuniyasu Suzaki, Masami Hagiya, Watcharin Leungwattanakit, Richard Potter, Eric Platon, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
- Journal Title
  
  International Journal of Networking and Computing
  
  Volume: 5 Issue: 2 Pages: 347-372
- DOI
  10.15803/ijnc.5.2_347
- NAID
  130005091738
- ISSN
  2185-2839, 2185-2847
- Language
  English
- Peer Reviewed / Acknowledgement Compliant / Open Access
- Data Source
  KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
[Journal Article] Using Checkpointing and Virtualization for Fault Injection2014
- Author(s)
  Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Eric Platon, Richard Potter, Kuniyasu Suzaki, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
- Journal Title
  
  Proc. Second International Symposium on Computing and Networking
  
  Volume: 2014 Pages: 144-150
- DOI
  10.1109/candar.2014.45
- NAID
  130005091738
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
[Journal Article] Software Model Checking of UDP-based Distributed Applications2014
- Author(s)
  Nazim Sebih, Franz Weitl, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
- Journal Title
  
  Proc. Second International Symposium on Computing and Networking
  
  Volume: 2014 Pages: 96-105
- DOI
  10.1109/candar.2014.66
- NAID
  130005091737
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
[Journal Article] Modular Software Model Checking for Distributed Systems2014
- Author(s)
  Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto, and Koichi Takahashi
- Journal Title
  
  IEEE Transactions on Software Engineering
  
  Volume: - Issue: 5 Pages: 483-501
- DOI
  10.1109/tse.2013.49
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-23300004
[Journal Article] Modbat: A Model-Based API Tester for Event-Driven Systems2013
- Author(s)
  Cyrille Valentin Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, and Mitsuharu Yamamoto
- Journal Title
  
  Proceedings of the 9th Haifa Verification Conference, Lecture Notes in Computer Science
  
  Volume: 8244 Pages: 112-128
- DOI
  10.1007/978-3-319-03077-7_8
- ISBN
  9783319030760, 9783319030777
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-23300004
[Journal Article] Software Model Checking for Distributed Systems with Selector-Based, Non-blocking Communication2013
- Author(s)
  Cyrille Artho, Masami Hagiya, Richard Potter, Yoshinori Tanabe, Franz Weitl, and Mitsuharu Yamamoto
- Journal Title
  
  28th IEEE/ACM International Conference on Automated Software Engineering
  
  Volume: - Pages: 169-179
- DOI
  10.1109/ase.2013.6693077
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-23300004, KAKENHI-PROJECT-23300011
[Journal Article] Model checking distributed systems by combining caching and process checkpointing2011
- Author(s)
  Watcharin Leungwattanakit
- Journal Title
  
  26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)
  
  Volume: 1 Pages: 103-112
- DOI
  10.1109/ase.2011.6100043
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21500006, KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-23300004, KAKENHI-PROJECT-23300011
[Journal Article] Model Checking of Concurrent Algorithms : From Java to C2010
- Author(s)
  Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Yoshinori Tanabe, Mitsuharu Yamamoto
- Journal Title
  
  IFIP Advances in Information and Communication Technology Vol.329
  
  Pages: 90-101
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20300006
[Journal Article] Model Checking of Concurrent Algorithms : From Java to C2010
- Author(s)
  Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Yoshinori Tanabe, Mitsuharu Yamamoto
- Journal Title
  
  IFIP Advances in Information and Communication Technology
  
  Volume: 329 Pages: 90-101
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20300006
[Journal Article] Model Checking of Concurrent Algorithms : From Java to C2010
- Author(s)
  Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Yoshinori Tanabe, Mitsuharu Yamamoto
- Journal Title
  
  DIPES 2010 : IFIP Conference on Distributed and Parallel Embedded Systems (掲載確定)
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20300006
[Journal Article] Cache-based Model Checking of Networked Applications : From Linear to Branching Time2009
- Author(s)
  Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
- Journal Title
  
  24th IEEE/ACM International Conference on Automated Software Engineering
  
  Pages: 447-458
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20300006
[Journal Article] Introduction of virtualization technology to multi-process model checking2009
- Author(s)
  Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
- Journal Title
  
  First NASA Formal Methods Symposium, NASA Conference Publication
  
  Pages: 106-110
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20300006
[Journal Article] Cache-based Model Checking of Networked Applicattions : From Linear to Branching Time2009
- Author(s)
  Cyrille Artho, Watcharin Leung wattanakit, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
- Journal Title
  
  24th IEEE/ACM International Conference on Automated Software Engineering
  
  Pages: 447-458
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20300006
[Journal Article] Verifying networked programs using a model checker extension2009
- Author(s)
  Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
- Journal Title
  
  31st International Conference on Software Engineering, Companion Volume
  
  Pages: 409-410
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20300006
[Journal Article] Model Checking of Multi-Process Applications Using SBUML and GDB2005
- Author(s)
  Yoshihiko Nakagawa, Richard Potter, Mitsuharu Yamamoto, Masami Hagiya, Kazuhiko Kato
- Journal Title
  
  Workshop on Dependable Software --Tools and Methods --,International Conference on dependable Systems and Networks
  
  Pages: 215-220
- Data Source
  KAKENHI-PROJECT-16016211
[Journal Article] BDDを用いた2方向CTL論理式充足可能性決定手続きの実装2005
- Author(s)
  田辺良則, 高橋孝一, 山本光晴, 佐藤貴洋, 萩谷昌己
- Journal Title
  
  コンピュータソフトウェア (掲載予定)
- NAID
  130004892028
- Data Source
  KAKENHI-PROJECT-16016211
[Journal Article] A Decision Procedure for the Alternation-free Two-way Modal mu-calculus2005
- Author(s)
  Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, Masami Hagiya
- Journal Title
  
  Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX),LNCS 3702
  
  Pages: 277-291
- Data Source
  KAKENHI-PROJECT-16016211
[Journal Article] BDDを用いた2方向CTL論理式充足可能性決定手続きの実装2005
- Author(s)
  田辺良則, 高橋孝一, 山本光晴, 佐藤貴洋, 萩谷昌己
- Journal Title
  
  コンピュータソフトウェア 22・3
  
  Pages: 154-166
- NAID
  130004892028
- Data Source
  KAKENHI-PROJECT-16016211
[Journal Article] A Decision Procedure for the Alternation-free Two-way Modal mu-calculus Automated Reasoning with Analytic Tableaux and Related Methods2005
- Author(s)
  Y.Tanabe, M.Yamamoto et al.
- Journal Title
  
  Lecture Note in Computer Science 3702
  
  Pages: 277-291
- Data Source
  KAKENHI-PROJECT-15540107
[Journal Article] Analysis of Synchronous and Asynchronous Cellular Automata using Abstraction by Temporal Logic2004
- Author(s)
  Masami Hagiya, Koichi Takahashi, Mitsuharu Yamamoto, et al.
- Journal Title
  
  Functional and Logic Programming (FLOPS 2004), LNCS 2998
  
  Pages: 7-21
- Data Source
  KAKENHI-PROJECT-16016211
[Journal Article] Analysis of Synchronous and Asynchronous Cellular Automata using Abstraction by Temporal Logic2004
- Author(s)
  Masami Hagiya, Mitsuharu Yamamoto
- Journal Title
  
  Lecture Notesin Computer Science 2998
  
  Pages: 7-21
- Data Source
  KAKENHI-PROJECT-15540107
[Journal Article] BDDを用いた2方向CTL論理式充足可能性決定手続きの実装
- Author(s)
  田辺良則, 山本光晴, 萩谷昌己
- Journal Title
  
  コンピュータソフトウェア (To appear)
- NAID
  130004892028
- Data Source
  KAKENHI-PROJECT-15540107
[Presentation] Coq/SSReflect/MathCompを用いたVASSからVASへの変換の形式化2024
- Author(s)
  脇坂勝大, 山本光晴
- Organizer
  第26回プログラミングおよびプログラミング言語ワークショップ（PPL 2024）
- Data Source
  KAKENHI-PROJECT-18K11154
[Presentation] VASSからVASへの変換の形式化2023
- Author(s)
  脇坂勝大, 山本光晴
- Organizer
  The 19th Theorem Proving and Provers meeting (TPP 2023)
- Data Source
  KAKENHI-PROJECT-18K11154
[Presentation] VASSからVASへの変換のMathCompによる形式化2023
- Author(s)
  脇坂勝大, 山本光晴
- Organizer
  日本ソフトウェア科学会第40回大会
- Data Source
  KAKENHI-PROJECT-18K11154
[Presentation] ペトリネットにおける停止性判定の形式化2019
- Author(s)
  稲垣衛, 山本光晴
- Organizer
  The 15th Theorem Proving and Provers meeting (TPP 2019)
- Data Source
  KAKENHI-PROJECT-18K11154
[Presentation] ペトリネットにおける有界性に関する性質のCoq/SSReflectによる形式化2019
- Author(s)
  稲垣衛, 山本光晴
- Organizer
  第21回プログラミングおよびプログラミング言語ワークショップ (PPL 2019)
- Data Source
  KAKENHI-PROJECT-18K11154
[Presentation] ニューラルネットワークにおける表現可能なデータ数のSSReflectによる形式化2019
- Author(s)
  井上健太, 山本光晴
- Organizer
  第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019) (ポスター)
- Data Source
  KAKENHI-PROJECT-16K00109
[Presentation] ペトリネットにおける有界性判定の形式化2018
- Author(s)
  稲垣衛, 山本光晴
- Organizer
  The 14th Theorem Proving and Provers meeting (TPP 2018)
- Data Source
  KAKENHI-PROJECT-18K11154
[Presentation] Monitoring Distributed Applications with Java Pathfinder2016
- Author(s)
  Lei Ma, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Alexander Kohan and Mitsuharu Yamamoto
- Organizer
  Java Pathfinder Workshop 2016
- Place of Presentation
  Seattle, USA
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-26280019
[Presentation] 3人の賢者の問題とその推論の妥当性のCoqにおける証明2016
- Author(s)
  井上健太，山本光晴
- Organizer
  第18回プログラミングおよびプログラミング言語ワークショップ（PPL2016）
- Place of Presentation
  ダイヤモンド瀬戸内マリンホテル (岡山県玉野市)
- Year and Date
  2016-03-08
- Data Source
  KAKENHI-PROJECT-25330096
[Presentation] GRT at the SBST 2015 Tool Competition2015
- Author(s)
  Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
- Organizer
  8th IEEE/ACM International Workshop on Search-Based Software Testing
- Place of Presentation
  フィレンツェ (イタリア)
- Year and Date
  2015-05-02
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-23240003
[Presentation] A formal proof of Higman's lemma in Coq/Ssreflect2015
- Author(s)
  M. Yamamoto
- Organizer
  11th Theorem Proving and Provers (TPP2015)
- Place of Presentation
  神奈川大学 (神奈川県平塚市)
- Year and Date
  2015-09-16
- Data Source
  KAKENHI-PROJECT-25330096
[Presentation] ペトリネットに対するKarp-Miller木構成のCoq/Ssreflectによる実装2015
- Author(s)
  松本早貴，山本光晴
- Organizer
  11th Theorem Proving and Provers (TPP2015)
- Place of Presentation
  神奈川大学 (神奈川県平塚市)
- Year and Date
  2015-09-16
- Data Source
  KAKENHI-PROJECT-25330096
[Presentation] Cardinality of UDP Transmission Outcomes2015
- Author(s)
  Franz Weitl, Nazim Sebih, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Mitsuharu Yamamoto
- Organizer
  1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications
- Place of Presentation
  南京 (中国)
- Year and Date
  2015-11-04
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-23240003
[Presentation] Software Model Checking for Distributed Systems with Selector-Based, Non-Blocking Communication2013
- Author(s)
  C. Artho, M. Hagiya, R. Potter, Y. Tanabe, F. Weitl, M. Yamamoto
- Organizer
  28th Int. Conf. on Automated Software Engineering
- Place of Presentation
  Crowne Plaza Cabana（米国、カリフォルニア州）
- Data Source
  KAKENHI-PROJECT-23240003
[Presentation] Modbat: A Model-based API Tester for Event-driven Systems2013
- Author(s)
  C. Artho, A. Biere, M. Hagiya, M. Seidl, E. Platon, Y. Tanabe, M. Yamamoto
- Organizer
  9th Haifa Verification Conference
- Place of Presentation
  IBM Research（イスラエル、Haifa）
- Data Source
  KAKENHI-PROJECT-23240003
[Presentation] Modbat: A model-based API tester for event-driven systems2012
- Author(s)
  C. Artho, A. Biere, M. Hagiya, R. Potter, R. Ramler, Y. Tanabe, F. Weitl, M. Yamamoto
- Organizer
  the Dependable Systems Workshop 2012
- Place of Presentation
  計算科学研究機構（兵庫）
- Data Source
  KAKENHI-PROJECT-23240003
[Presentation] Model Checking Distributed Systems by Combining Caching and Process Checkpointing2011
- Author(s)
  W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto
- Organizer
  26th Int. Conf. on Automated Software Engineering (ASE 2011)
- Place of Presentation
  Oread, Lawrence, Kan, USA
- Data Source
  KAKENHI-PROJECT-23240003
[Presentation] ネットワークアプリケーションのマスター・スレーブ方式モデル検査アルゴリズムについて2011
- Author(s)
  田辺良則, Cyriile Artho, Watcharin Leungwattanakit, 山本光晴, 萩谷昌己
- Organizer
  日本ソフトウェア科学会第28回大会
- Place of Presentation
  沖縄産業支援センター，沖縄県那覇市
- Data Source
  KAKENHI-PROJECT-23240003
[Presentation] SSReflectを用いたペトリネットにおけるカープミラー加速の形式化
- Author(s)
  関根祥吾, 山本光晴
- Organizer
  Theorem proving and provers for reliable theory and implementations (TPP2014)
- Place of Presentation
  九州大学・西新プラザ大会議室 (福岡県)
- Year and Date
  2014-12-03 – 2014-12-05
- Data Source
  KAKENHI-PROJECT-25330096
[Presentation] Using Checkpointing and Virtualization for Fault Injection
- Author(s)
  Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Eric Platon, Richard Potter, Kuniyasu Suzaki, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
- Organizer
  The Second International Symposium on Computing and Networking (CANDAR 2014)
- Place of Presentation
  静岡県コンベンションアーツセンター (静岡県)
- Year and Date
  2014-12-10 – 2014-12-12
- Data Source
  KAKENHI-PROJECT-23240003
[Presentation] Software Model Checking of UDP-based Distributed Applications
- Author(s)
  Nazim Sebih, Franz Weitl, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
- Organizer
  The Second International Symposium on Computing and Networking (CANDAR 2014)
- Place of Presentation
  静岡県コンベンションアーツセンター (静岡県)
- Year and Date
  2014-12-10 – 2014-12-12
- Data Source
  KAKENHI-PROJECT-23240003

1. HAGIYA Masami (30156252)

# of Collaborated Projects: 11 results

# of Collaborated Products: 33 results
2. TANABE Yoshinori (60443199)

# of Collaborated Projects: 6 results

# of Collaborated Products: 28 results
3. SAKURAI Takafumi (60183373)

# of Collaborated Projects: 5 results

# of Collaborated Products: 0 results
4. TSUJI Takashi (70016666)

# of Collaborated Projects: 5 results

# of Collaborated Products: 0 results
5. KOMORI Yuichi (10022302)

# of Collaborated Projects: 5 results

# of Collaborated Products: 0 results
6. ARTHO Cyrille (30462831)

# of Collaborated Projects: 4 results

# of Collaborated Products: 28 results
7. TAKAHASHI Koichi (40357372)

# of Collaborated Projects: 4 results

# of Collaborated Products: 0 results
8. WEITL Franz

# of Collaborated Projects: 3 results

# of Collaborated Products: 10 results
9. HIROKAWA Sachiko (40126785)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
10. TAGURI Masaaki (10009607)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
11. KONNO Yoshihiko (00205577)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
12. NAKAGAMI Junichi (30092076)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
13. FUJITA Ken-etsu (30228994)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
14. POTTER Richard

# of Collaborated Projects: 2 results

# of Collaborated Products: 5 results
15. LEUNGWATTANAKIT Watcharin

# of Collaborated Projects: 2 results

# of Collaborated Products: 5 results
16. SEBIH Nazim

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
17. YOKOYAMA Shigetoshi (10600968)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
18. TANEMURA Hideki (40217162)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
19. HASHIMOTO Akihiro (60164779)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
20. MIYANO Hisao (90200196)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
21. KANAZAWA Makoto (20261886)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
22. TAMAI Tetsuo (60217172)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
23. SHIRAISHI Taka-aki (50143160)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
24. TAKIZAWA Yumi (90280528)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
25. KASHIMA Ryo (10240756)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
26. 山形頼之 (40415758)

# of Collaborated Projects: 1 results

# of Collaborated Products: 3 results
27. 渚勝 (50189172)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
28. 中村吉邑 (90110270)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
29. 西崎真也 (90263615)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
30. 腰越秀之 (70110294)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
31. 中神祥臣 (70091246)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
32. 峰村勝弘 (20060684)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
33. 安田正実 (00041244)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
34. 多田充 (20303331)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
35. YUASA Yoshifumi

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
36. HENMI Ko

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
37. KOHAN Alexander

# of Collaborated Projects: 1 results

# of Collaborated Products: 2 results
38. MA Lei

# of Collaborated Projects: 1 results

# of Collaborated Products: 4 results

Yamamoto Mitsuharu 山本 光晴

YAMAMOTO Mitsuharu 山本 光晴

Research Projects

Research Products

Co-Researchers

Formalization of the decidability of the reachability problem for vector addition systemsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Integrated Runtime Monitoring of Network Software by Fusion of Runtime Verification and Model CheckingPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Model Checking Network Applications using Distributed CheckpointingPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Communication Backtracking by Virtual Machines and Applications to Model CheckingPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Principal Investigator

Project Period (FY)

Yamamoto Mitsuharu 山本光晴

YAMAMOTO Mitsuharu 山本光晴