Yamamoto Mitsuharu 山本光晴

… Alternative Names

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

Formalization of the decidability of the reachability problem for vector addition systemsPrincipal InvestigatorOngoing
- Principal Investigator
  
  山本光晴
- Project Period (FY)
  2018 – 2022
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Chiba University
ソフトウェアモデル検査における活性検証Ongoing
- Principal Investigator
  
  田辺良則
- 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

All 2017 2016 2015 2014 2013 2012 2011 2010 2009 2005 2004 Other

All Journal Article Presentation

[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: 印刷中
- Acknowledgement Compliant / Open Access / Peer Reviewed
- 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
- Acknowledgement Compliant / Peer Reviewed
- 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
- Open Access / Acknowledgement Compliant / Peer Reviewed
- 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) Pages: 1-5
- DOI
  10.1145/3011286.3011292
- Open Access / Acknowledgement Compliant / Peer Reviewed
- 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
  
  IEEE/ACM 8th International Workshop on Search-Based Software Testing
  
  Volume: 2015 Pages: 48-51
- DOI
  10.1109/sbst.2015.19
- Open Access / Int'l Joint Research / Peer Reviewed
- 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
  
  Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015
  
  Volume: 2015 Pages: 120-134
- DOI
  10.1007/978-3-319-25942-0_8
- Open Access / Acknowledgement Compliant / Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
[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
- Language
  English
- Peer Reviewed / Open Access / Acknowledgement Compliant
- 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: Vol. 5, No. 2 Issue: 2 Pages: 373-402
- DOI
  10.15803/ijnc.5.2_373
- Language
  English
- Peer Reviewed / Open Access / Acknowledgement Compliant
- 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 Pages: 373-402
- Open Access / Acknowledgement Compliant / Peer Reviewed
- Data Source
  KAKENHI-PROJECT-23240003
[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
  
  Second International Symposium on Computing and Networking (CANDAR), 2014
  
  Volume: 2014 Pages: 144-150
- DOI
  10.1109/candar.2014.45
- 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
  
  Second International Symposium on Computing and Networking (CANDAR), 2014
  
  Volume: 2014 Pages: 96-105
- DOI
  10.1109/candar.2014.66
- 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: - 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
  
  Hardware and Software: Verification and Testing, 9th International Haifa Verification Conference, HVC 2013, Haifa, Israel, November 5-7, 2013, Proceedings
  
  Volume: 8244 Pages: 112-128
- DOI
  10.1007/978-3-319-03077-7_8
- 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
  
  ASE
  
  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] Mitsuharu Yamamoto : Model checking distributed systems by combining caching and process checkpointing2011
- Author(s)
  Watcharin Leungwattanakit
- Journal Title
  
  ASE
  
  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
  
  コンピュータソフトウェア (掲載予定)
- 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
- 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)
- Data Source
  KAKENHI-PROJECT-15540107
[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: 36 results
2. TANABE Yoshinori (60443199)

# of Collaborated Projects: 6 results

# of Collaborated Products: 31 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: 31 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: 17 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: 7 results
15. LEUNGWATTANAKIT Watcharin

# of Collaborated Projects: 2 results

# of Collaborated Products: 9 results
16. SEBIH Nazim

# of Collaborated Projects: 2 results

# of Collaborated Products: 3 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: 0 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: 10 results

Yamamoto Mitsuharu 山本 光晴

YAMAMOTO Mitsuharu 山本 光晴

Research Projects

Research Products

Co-Researchers

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

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

ソフトウェアモデル検査における活性検証Ongoing

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

Yamamoto Mitsuharu 山本光晴

YAMAMOTO Mitsuharu 山本光晴