• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

山本 光晴  Yamamoto Mitsuharu

ORCIDORCID連携する *注記
研究者番号 00291295
その他のID
所属 (現在) 2025年度: 千葉大学, 大学院理学研究院, 教授
所属 (過去の研究課題情報に基づく) *注記 2017年度 – 2023年度: 千葉大学, 大学院理学研究院, 教授
2014年度 – 2016年度: 千葉大学, 大学院理学研究科, 准教授
2011年度 – 2016年度: 千葉大学, 理学(系)研究科(研究院), 准教授
2008年度 – 2011年度: 千葉大学, 大学院・理学研究科, 准教授
2003年度 – 2006年度: 千葉大学, 理学部, 助教授
1998年度 – 2002年度: 千葉大学, 理学部, 助手
審査区分/研究分野
研究代表者
理工系 / ソフトウエア / 小区分60010:情報学基礎論関連 / ソフトウェア
研究代表者以外
計算機科学 / 統計科学 / ソフトウェア / 数学一般(含確率論・統計数学) / 数学一般(含確率論・統計数学) / ソフトウエア
キーワード
研究代表者
証明検証系 / 形式的手法 / グラフ書き換え / 抽象モデル検査 / モデル検査 / チェックポインティング / セルオートマトン / 時相論理 / 時間ペトリネット / 時間付きオートマトン … もっと見る / 時間付き多重集合書き換え / ペトリネット / 到達可能性 / ベクトル加算系 / 形式化 / 定理証明支援系 / ネットワークソフトウェア / 実行時検証 / 実環境モデル検査 / 仮想計算機 / グラフ探索 … もっと見る
研究代表者以外
部分構造論理 / 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 / ディペンダブル・コンピューティング / 定理証明支援系 / クラウドコンピューティング / ソフトウェアモデル検査 / 仕様記述・仕様検証 隠す
  • 研究課題

    (18件)
  • 研究成果

    (51件)
  • 共同研究者

    (38人)
  •  ベクトル加算系における到達可能性問題の決定可能性の形式化研究代表者

    • 研究代表者
      山本 光晴
    • 研究期間 (年度)
      2018 – 2023
    • 研究種目
      基盤研究(C)
    • 審査区分
      小区分60010:情報学基礎論関連
    • 研究機関
      千葉大学
  •  ソフトウェアモデル検査における活性検証

    • 研究代表者
      田辺 良則
    • 研究期間 (年度)
      2016 – 2018
    • 研究種目
      基盤研究(C)
    • 研究分野
      ソフトウェア
    • 研究機関
      鶴見大学
  •  実行時検証とモデル検査の融合によるネットワークソフトウェアの統合実行監視研究代表者

    • 研究代表者
      山本 光晴
    • 研究期間 (年度)
      2014 – 2016
    • 研究種目
      基盤研究(B)
    • 研究分野
      ソフトウェア
    • 研究機関
      千葉大学
  •  定理証明器によるモジュラーなソフトウェア検証

    • 研究代表者
      田辺 良則
    • 研究期間 (年度)
      2013 – 2015
    • 研究種目
      基盤研究(C)
    • 研究分野
      ソフトウェア
    • 研究機関
      鶴見大学
      国立情報学研究所
  •  クラウドコンピューティングミドルウェアのソフトウェアモデル検査手法

    • 研究代表者
      萩谷 昌己
    • 研究期間 (年度)
      2011 – 2015
    • 研究種目
      基盤研究(A)
    • 研究分野
      ソフトウエア
    • 研究機関
      東京大学
  •  分散チェックポインティングを用いたネットワークアプリケーションのモデル検査研究代表者

    • 研究代表者
      山本 光晴
    • 研究期間 (年度)
      2011 – 2013
    • 研究種目
      基盤研究(B)
    • 研究分野
      ソフトウエア
    • 研究機関
      千葉大学
  •  仮想計算機によるコミュニケーションバックトラッキングとモデル検査への応用研究代表者

    • 研究代表者
      山本 光晴
    • 研究期間 (年度)
      2008 – 2010
    • 研究種目
      基盤研究(B)
    • 研究分野
      ソフトウエア
    • 研究機関
      千葉大学
  •  抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証研究代表者

    • 研究代表者
      山本 光晴
    • 研究期間 (年度)
      2004 – 2005
    • 研究種目
      特定領域研究
    • 審査区分
      理工系
    • 研究機関
      千葉大学
  •  抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証研究代表者

    • 研究代表者
      山本 光晴
    • 研究期間 (年度)
      2003
    • 研究種目
      特定領域研究
    • 審査区分
      理工系
    • 研究機関
      千葉大学
  •  チャーチのラムダ計算のBCK論理による再生

    • 研究代表者
      古森 雄一
    • 研究期間 (年度)
      2003 – 2006
    • 研究種目
      基盤研究(C)
    • 研究分野
      数学一般(含確率論・統計数学)
    • 研究機関
      千葉大学
  •  抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証研究代表者

    • 研究代表者
      山本 光晴
    • 研究期間 (年度)
      2002
    • 研究種目
      特定領域研究
    • 審査区分
      理工系
    • 研究機関
      千葉大学
  •  抽象モデル検査のためのグラフ探索アルゴリズムの形式化と検証研究代表者

    • 研究代表者
      山本 光晴
    • 研究期間 (年度)
      2001
    • 研究種目
      特定領域研究(C)
    • 審査区分
      理工系
    • 研究機関
      千葉大学
  •  スタイン現象および縮小推定法の新展開

    • 研究代表者
      今野 良彦
    • 研究期間 (年度)
      2001 – 2004
    • 研究種目
      基盤研究(C)
    • 研究分野
      統計科学
    • 研究機関
      日本女子大学
      千葉大学
  •  論理体系の意味論と文法的性質の関係

    • 研究代表者
      桜井 貴文
    • 研究期間 (年度)
      2000 – 2001
    • 研究種目
      基盤研究(C)
    • 研究分野
      計算機科学
    • 研究機関
      千葉大学
  •  描象モデル検査とその応用

    • 研究代表者
      萩谷 昌己
    • 研究期間 (年度)
      1999 – 2001
    • 研究種目
      基盤研究(B)
    • 研究分野
      計算機科学
    • 研究機関
      東京大学
  •  状態空間モデルに基づく縦断的データの解析へのブートストラップ法による接近

    • 研究代表者
      田栗 正章
    • 研究期間 (年度)
      1998 – 2000
    • 研究種目
      基盤研究(B)
    • 研究分野
      統計科学
    • 研究機関
      千葉大学
  •  部分構造論理の研究

    • 研究代表者
      古森 雄一
    • 研究期間 (年度)
      1998 – 1999
    • 研究種目
      基盤研究(C)
    • 研究分野
      数学一般(含確率論・統計数学)
    • 研究機関
      千葉大学
  •  型理論の意味論と文法的性質の関係

    • 研究代表者
      桜井 貴文
    • 研究期間 (年度)
      1998 – 1999
    • 研究種目
      基盤研究(C)
    • 研究分野
      計算機科学
    • 研究機関
      千葉大学

すべて 2024 2023 2019 2018 2017 2016 2015 2014 2013 2012 2011 2010 2009 2005 2004 その他

すべて 雑誌論文 学会発表

  • [雑誌論文] Model-based API Testing of Apache ZooKeeper2017

    • 著者名/発表者名
      Cyrille Valentin Artho, Quentin Gros, Guillaume Rousset, Kazuaki Banzai, Lei Ma, Takashi Kitamura, Masami Hagiya, Yoshinori Tanabe, and Mitsuharu Yamamoto
    • 雑誌名

      10th IEEE International Conference on Software Testing, Verification and Validation (ICST 2017)

      巻: 印刷中

    • 査読あり / 謝辞記載あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-26280019
  • [雑誌論文] Formalization of Karp-Miller tree construction on petri nets2017

    • 著者名/発表者名
      Mitsuharu Yamamoto, Shogo Sekine, Saki Matsumoto
    • 雑誌名

      Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

      巻: - ページ: 66-78

    • DOI

      10.1145/3018610.3018626

    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-16K00109
  • [雑誌論文] Runtime Monitoring for Concurrent Systems2016

    • 著者名/発表者名
      Yoriyuki Yamagata, Cyrille Artho, Masami Hagiya, Jun Inoue, Lei Ma, Yoshinori Tanabe, and Mitsuharu Yamamoto
    • 雑誌名

      Runtime Verification - 16th International Conference, (RV 2016)

      巻: LNCS 10012 ページ: 386-403

    • DOI

      10.1007/978-3-319-46982-9_24

    • ISBN
      9783319469812, 9783319469829
    • 査読あり / 謝辞記載あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-26280019
  • [雑誌論文] Java Pathfinder on Android Devices2016

    • 著者名/発表者名
      Alexander Kohan, Mitsuharu Yamamoto, Cyrille Artho, Yoriyuki Yamagata, Lei Ma, Masami Hagiya, and Yoshinori Tanabe
    • 雑誌名

      ACM SIGSOFT Software Engineering Notes

      巻: 41(6) 号: 6 ページ: 1-5

    • DOI

      10.1145/3011286.3011292

    • 査読あり / 謝辞記載あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-26280019
  • [雑誌論文] Software Model Checking of UDP-based Distributed Applications2015

    • 著者名/発表者名
      Nazim Sebih, Masami Hagiya, Franz Weitl, Mitsuharu Yamamoto, Cyrille Artho, Yoshinori Tanabe
    • 雑誌名

      International Journal of Networking and Computing

      巻: 5 号: 2 ページ: 373-402

    • DOI

      10.15803/ijnc.5.2_373

    • NAID

      130005091737

    • ISSN
      2185-2839, 2185-2847
    • 言語
      英語
    • 査読あり / 謝辞記載あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-26280019
  • [雑誌論文] GRT at the SBST 2015 Tool Competition2015

    • 著者名/発表者名
      Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 雑誌名

      Proc 8th IEEE/ACM International Workshop on Search-Based Software Testing

      巻: 2015 ページ: 48-51

    • DOI

      10.1109/sbst.2015.19

    • 査読あり / オープンアクセス / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
  • [雑誌論文] Cardinality of UDP Transmission Outcomes2015

    • 著者名/発表者名
      Franz Weitl, Nazim Sebih, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Mitsuharu Yamamoto
    • 雑誌名

      Proc 1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications

      巻: 2015 ページ: 120-134

    • DOI

      10.1007/978-3-319-25942-0_8

    • ISBN
      9783319259413, 9783319259420
    • 査読あり / 謝辞記載あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
  • [雑誌論文] Software Model Checking of UDP-based Distributed Applications2015

    • 著者名/発表者名
      Nazim Sebih, Masami Hagiya, Franz Weitl, Mitsuharu Yamamoto, Cyrille Artho, Yoshinori Tanabe
    • 雑誌名

      International Journal of Networking and Computing

      巻: 5 ページ: 373-402

    • NAID

      130005091737

    • 査読あり / 謝辞記載あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-23240003
  • [雑誌論文] Using Checkpointing and Virtualization for Fault Injection2015

    • 著者名/発表者名
      Cyrille Artho, Kuniyasu Suzaki, Masami Hagiya, Watcharin Leungwattanakit, Richard Potter, Eric Platon, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
    • 雑誌名

      International Journal of Networking and Computing

      巻: 5 号: 2 ページ: 347-372

    • DOI

      10.15803/ijnc.5.2_347

    • NAID

      130005091738

    • ISSN
      2185-2839, 2185-2847
    • 言語
      英語
    • 査読あり / 謝辞記載あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
  • [雑誌論文] Using Checkpointing and Virtualization for Fault Injection2014

    • 著者名/発表者名
      Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Eric Platon, Richard Potter, Kuniyasu Suzaki, Yoshinori Tanabe, Franz Weitl, Mitsuharu Yamamoto
    • 雑誌名

      Proc. Second International Symposium on Computing and Networking

      巻: 2014 ページ: 144-150

    • DOI

      10.1109/candar.2014.45

    • NAID

      130005091738

    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
  • [雑誌論文] Software Model Checking of UDP-based Distributed Applications2014

    • 著者名/発表者名
      Nazim Sebih, Franz Weitl, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 雑誌名

      Proc. Second International Symposium on Computing and Networking

      巻: 2014 ページ: 96-105

    • DOI

      10.1109/candar.2014.66

    • NAID

      130005091737

    • 査読あり
    • データソース
      KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-26280019
  • [雑誌論文] Modular Software Model Checking for Distributed Systems2014

    • 著者名/発表者名
      Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto, and Koichi Takahashi
    • 雑誌名

      IEEE Transactions on Software Engineering

      巻: - 号: 5 ページ: 483-501

    • DOI

      10.1109/tse.2013.49

    • 査読あり
    • データソース
      KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-23300004
  • [雑誌論文] Modbat: A Model-Based API Tester for Event-Driven Systems2013

    • 著者名/発表者名
      Cyrille Valentin Artho, Armin Biere, Masami Hagiya, Eric Platon, Martina Seidl, Yoshinori Tanabe, and Mitsuharu Yamamoto
    • 雑誌名

      Proceedings of the 9th Haifa Verification Conference, Lecture Notes in Computer Science

      巻: 8244 ページ: 112-128

    • DOI

      10.1007/978-3-319-03077-7_8

    • ISBN
      9783319030760, 9783319030777
    • 査読あり
    • データソース
      KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-23300004
  • [雑誌論文] Software Model Checking for Distributed Systems with Selector-Based, Non-blocking Communication2013

    • 著者名/発表者名
      Cyrille Artho, Masami Hagiya, Richard Potter, Yoshinori Tanabe, Franz Weitl, and Mitsuharu Yamamoto
    • 雑誌名

      28th IEEE/ACM International Conference on Automated Software Engineering

      巻: - ページ: 169-179

    • DOI

      10.1109/ase.2013.6693077

    • 査読あり
    • データソース
      KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-23300004, KAKENHI-PROJECT-23300011
  • [雑誌論文] Model checking distributed systems by combining caching and process checkpointing2011

    • 著者名/発表者名
      Watcharin Leungwattanakit
    • 雑誌名

      26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011)

      巻: 1 ページ: 103-112

    • DOI

      10.1109/ase.2011.6100043

    • 査読あり
    • データソース
      KAKENHI-PROJECT-21500006, KAKENHI-PROJECT-23240003, KAKENHI-PROJECT-23300004, KAKENHI-PROJECT-23300011
  • [雑誌論文] Model Checking of Concurrent Algorithms : From Java to C2010

    • 著者名/発表者名
      Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 雑誌名

      IFIP Advances in Information and Communication Technology Vol.329

      ページ: 90-101

    • 査読あり
    • データソース
      KAKENHI-PROJECT-20300006
  • [雑誌論文] Model Checking of Concurrent Algorithms : From Java to C2010

    • 著者名/発表者名
      Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 雑誌名

      IFIP Advances in Information and Communication Technology

      巻: 329 ページ: 90-101

    • 査読あり
    • データソース
      KAKENHI-PROJECT-20300006
  • [雑誌論文] Model Checking of Concurrent Algorithms : From Java to C2010

    • 著者名/発表者名
      Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 雑誌名

      DIPES 2010 : IFIP Conference on Distributed and Parallel Embedded Systems (掲載確定)

    • 査読あり
    • データソース
      KAKENHI-PROJECT-20300006
  • [雑誌論文] Cache-based Model Checking of Networked Applications : From Linear to Branching Time2009

    • 著者名/発表者名
      Cyrille Artho, Watcharin Leungwattanakit, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 雑誌名

      24th IEEE/ACM International Conference on Automated Software Engineering

      ページ: 447-458

    • 査読あり
    • データソース
      KAKENHI-PROJECT-20300006
  • [雑誌論文] Introduction of virtualization technology to multi-process model checking2009

    • 著者名/発表者名
      Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 雑誌名

      First NASA Formal Methods Symposium, NASA Conference Publication

      ページ: 106-110

    • 査読あり
    • データソース
      KAKENHI-PROJECT-20300006
  • [雑誌論文] Cache-based Model Checking of Networked Applicattions : From Linear to Branching Time2009

    • 著者名/発表者名
      Cyrille Artho, Watcharin Leung wattanakit, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 雑誌名

      24th IEEE/ACM International Conference on Automated Software Engineering

      ページ: 447-458

    • 査読あり
    • データソース
      KAKENHI-PROJECT-20300006
  • [雑誌論文] Verifying networked programs using a model checker extension2009

    • 著者名/発表者名
      Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 雑誌名

      31st International Conference on Software Engineering, Companion Volume

      ページ: 409-410

    • 査読あり
    • データソース
      KAKENHI-PROJECT-20300006
  • [雑誌論文] Model Checking of Multi-Process Applications Using SBUML and GDB2005

    • 著者名/発表者名
      Yoshihiko Nakagawa, Richard Potter, Mitsuharu Yamamoto, Masami Hagiya, Kazuhiko Kato
    • 雑誌名

      Workshop on Dependable Software --Tools and Methods --,International Conference on dependable Systems and Networks

      ページ: 215-220

    • データソース
      KAKENHI-PROJECT-16016211
  • [雑誌論文] BDDを用いた2方向CTL論理式充足可能性決定手続きの実装2005

    • 著者名/発表者名
      田辺良則, 高橋孝一, 山本光晴, 佐藤貴洋, 萩谷昌己
    • 雑誌名

      コンピュータソフトウェア (掲載予定)

    • NAID

      130004892028

    • データソース
      KAKENHI-PROJECT-16016211
  • [雑誌論文] A Decision Procedure for the Alternation-free Two-way Modal mu-calculus2005

    • 著者名/発表者名
      Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, Masami Hagiya
    • 雑誌名

      Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX),LNCS 3702

      ページ: 277-291

    • データソース
      KAKENHI-PROJECT-16016211
  • [雑誌論文] BDDを用いた2方向CTL論理式充足可能性決定手続きの実装2005

    • 著者名/発表者名
      田辺良則, 高橋孝一, 山本光晴, 佐藤貴洋, 萩谷昌己
    • 雑誌名

      コンピュータソフトウェア 22・3

      ページ: 154-166

    • NAID

      130004892028

    • データソース
      KAKENHI-PROJECT-16016211
  • [雑誌論文] A Decision Procedure for the Alternation-free Two-way Modal mu-calculus Automated Reasoning with Analytic Tableaux and Related Methods2005

    • 著者名/発表者名
      Y.Tanabe, M.Yamamoto et al.
    • 雑誌名

      Lecture Note in Computer Science 3702

      ページ: 277-291

    • データソース
      KAKENHI-PROJECT-15540107
  • [雑誌論文] Analysis of Synchronous and Asynchronous Cellular Automata using Abstraction by Temporal Logic2004

    • 著者名/発表者名
      Masami Hagiya, Koichi Takahashi, Mitsuharu Yamamoto, et al.
    • 雑誌名

      Functional and Logic Programming (FLOPS 2004), LNCS 2998

      ページ: 7-21

    • データソース
      KAKENHI-PROJECT-16016211
  • [雑誌論文] Analysis of Synchronous and Asynchronous Cellular Automata using Abstraction by Temporal Logic2004

    • 著者名/発表者名
      Masami Hagiya, Mitsuharu Yamamoto
    • 雑誌名

      Lecture Notesin Computer Science 2998

      ページ: 7-21

    • データソース
      KAKENHI-PROJECT-15540107
  • [雑誌論文] BDDを用いた2方向CTL論理式充足可能性決定手続きの実装

    • 著者名/発表者名
      田辺良則, 山本光晴, 萩谷昌己
    • 雑誌名

      コンピュータソフトウェア (To appear)

    • NAID

      130004892028

    • データソース
      KAKENHI-PROJECT-15540107
  • [学会発表] Coq/SSReflect/MathCompを用いたVASSからVASへの変換の形式化2024

    • 著者名/発表者名
      脇坂 勝大, 山本 光晴
    • 学会等名
      第26回プログラミングおよびプログラミング言語ワークショップ(PPL 2024)
    • データソース
      KAKENHI-PROJECT-18K11154
  • [学会発表] VASSからVASへの変換の形式化2023

    • 著者名/発表者名
      脇坂 勝大, 山本 光晴
    • 学会等名
      The 19th Theorem Proving and Provers meeting (TPP 2023)
    • データソース
      KAKENHI-PROJECT-18K11154
  • [学会発表] VASSからVASへの変換のMathCompによる形式化2023

    • 著者名/発表者名
      脇坂 勝大, 山本 光晴
    • 学会等名
      日本ソフトウェア科学会第40回大会
    • データソース
      KAKENHI-PROJECT-18K11154
  • [学会発表] ペトリネットにおける停止性判定の形式化2019

    • 著者名/発表者名
      稲垣 衛, 山本 光晴
    • 学会等名
      The 15th Theorem Proving and Provers meeting (TPP 2019)
    • データソース
      KAKENHI-PROJECT-18K11154
  • [学会発表] ペトリネットにおける有界性に関する性質のCoq/SSReflectによる形式化2019

    • 著者名/発表者名
      稲垣 衛, 山本 光晴
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ (PPL 2019)
    • データソース
      KAKENHI-PROJECT-18K11154
  • [学会発表] ニューラルネットワークにおける表現可能なデータ数のSSReflectによる形式化2019

    • 著者名/発表者名
      井上健太, 山本光晴
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019) (ポスター)
    • データソース
      KAKENHI-PROJECT-16K00109
  • [学会発表] ペトリネットにおける有界性判定の形式化2018

    • 著者名/発表者名
      稲垣 衛, 山本 光晴
    • 学会等名
      The 14th Theorem Proving and Provers meeting (TPP 2018)
    • データソース
      KAKENHI-PROJECT-18K11154
  • [学会発表] Monitoring Distributed Applications with Java Pathfinder2016

    • 著者名/発表者名
      Lei Ma, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Alexander Kohan and Mitsuharu Yamamoto
    • 学会等名
      Java Pathfinder Workshop 2016
    • 発表場所
      Seattle, USA
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-26280019
  • [学会発表] 3人の賢者の問題とその推論の妥当性のCoqにおける証明2016

    • 著者名/発表者名
      井上健太,山本光晴
    • 学会等名
      第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)
    • 発表場所
      ダイヤモンド瀬戸内マリンホテル (岡山県玉野市)
    • 年月日
      2016-03-08
    • データソース
      KAKENHI-PROJECT-25330096
  • [学会発表] GRT at the SBST 2015 Tool Competition2015

    • 著者名/発表者名
      Lei Ma, Cyrille Artho, Cheng Zhang, Hiroyuki Sato, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 学会等名
      8th IEEE/ACM International Workshop on Search-Based Software Testing
    • 発表場所
      フィレンツェ (イタリア)
    • 年月日
      2015-05-02
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-23240003
  • [学会発表] A formal proof of Higman's lemma in Coq/Ssreflect2015

    • 著者名/発表者名
      M. Yamamoto
    • 学会等名
      11th Theorem Proving and Provers (TPP2015)
    • 発表場所
      神奈川大学 (神奈川県平塚市)
    • 年月日
      2015-09-16
    • データソース
      KAKENHI-PROJECT-25330096
  • [学会発表] ペトリネットに対するKarp-Miller木構成のCoq/Ssreflectによる実装2015

    • 著者名/発表者名
      松本早貴,山本光晴
    • 学会等名
      11th Theorem Proving and Provers (TPP2015)
    • 発表場所
      神奈川大学 (神奈川県平塚市)
    • 年月日
      2015-09-16
    • データソース
      KAKENHI-PROJECT-25330096
  • [学会発表] Cardinality of UDP Transmission Outcomes2015

    • 著者名/発表者名
      Franz Weitl, Nazim Sebih, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Yoriyuki Yamagata, Mitsuharu Yamamoto
    • 学会等名
      1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications
    • 発表場所
      南京 (中国)
    • 年月日
      2015-11-04
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-23240003
  • [学会発表] Software Model Checking for Distributed Systems with Selector-Based, Non-Blocking Communication2013

    • 著者名/発表者名
      C. Artho, M. Hagiya, R. Potter, Y. Tanabe, F. Weitl, M. Yamamoto
    • 学会等名
      28th Int. Conf. on Automated Software Engineering
    • 発表場所
      Crowne Plaza Cabana(米国、カリフォルニア州)
    • データソース
      KAKENHI-PROJECT-23240003
  • [学会発表] Modbat: A Model-based API Tester for Event-driven Systems2013

    • 著者名/発表者名
      C. Artho, A. Biere, M. Hagiya, M. Seidl, E. Platon, Y. Tanabe, M. Yamamoto
    • 学会等名
      9th Haifa Verification Conference
    • 発表場所
      IBM Research(イスラエル、Haifa)
    • データソース
      KAKENHI-PROJECT-23240003
  • [学会発表] Modbat: A model-based API tester for event-driven systems2012

    • 著者名/発表者名
      C. Artho, A. Biere, M. Hagiya, R. Potter, R. Ramler, Y. Tanabe, F. Weitl, M. Yamamoto
    • 学会等名
      the Dependable Systems Workshop 2012
    • 発表場所
      計算科学研究機構(兵庫)
    • データソース
      KAKENHI-PROJECT-23240003
  • [学会発表] Model Checking Distributed Systems by Combining Caching and Process Checkpointing2011

    • 著者名/発表者名
      W. Leungwattanakit, C. Artho, M. Hagiya, Y. Tanabe, M. Yamamoto
    • 学会等名
      26th Int. Conf. on Automated Software Engineering (ASE 2011)
    • 発表場所
      Oread, Lawrence, Kan, USA
    • データソース
      KAKENHI-PROJECT-23240003
  • [学会発表] ネットワークアプリケーションのマスター・スレーブ方式モデル検査アルゴリズムについて2011

    • 著者名/発表者名
      田辺 良則, Cyriile Artho, Watcharin Leungwattanakit, 山本 光晴, 萩谷 昌己
    • 学会等名
      日本ソフトウェア科学会第28回大会
    • 発表場所
      沖縄産業支援センター,沖縄県那覇市
    • データソース
      KAKENHI-PROJECT-23240003
  • [学会発表] SSReflectを用いたペトリネットにおけるカープミラー加速の形式化

    • 著者名/発表者名
      関根祥吾, 山本光晴
    • 学会等名
      Theorem proving and provers for reliable theory and implementations (TPP2014)
    • 発表場所
      九州大学・西新プラザ大会議室 (福岡県)
    • 年月日
      2014-12-03 – 2014-12-05
    • データソース
      KAKENHI-PROJECT-25330096
  • [学会発表] 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
    • 学会等名
      The Second International Symposium on Computing and Networking (CANDAR 2014)
    • 発表場所
      静岡県コンベンションアーツセンター (静岡県)
    • 年月日
      2014-12-10 – 2014-12-12
    • データソース
      KAKENHI-PROJECT-23240003
  • [学会発表] Software Model Checking of UDP-based Distributed Applications

    • 著者名/発表者名
      Nazim Sebih, Franz Weitl, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, Mitsuharu Yamamoto
    • 学会等名
      The Second International Symposium on Computing and Networking (CANDAR 2014)
    • 発表場所
      静岡県コンベンションアーツセンター (静岡県)
    • 年月日
      2014-12-10 – 2014-12-12
    • データソース
      KAKENHI-PROJECT-23240003
  • 1.  萩谷 昌己 (30156252)
    共同の研究課題数: 11件
    共同の研究成果数: 33件
  • 2.  田辺 良則 (60443199)
    共同の研究課題数: 6件
    共同の研究成果数: 28件
  • 3.  桜井 貴文 (60183373)
    共同の研究課題数: 5件
    共同の研究成果数: 0件
  • 4.  辻 尚史 (70016666)
    共同の研究課題数: 5件
    共同の研究成果数: 0件
  • 5.  古森 雄一 (10022302)
    共同の研究課題数: 5件
    共同の研究成果数: 0件
  • 6.  アルト シリル (30462831)
    共同の研究課題数: 4件
    共同の研究成果数: 28件
  • 7.  高橋 孝一 (40357372)
    共同の研究課題数: 4件
    共同の研究成果数: 0件
  • 8.  ヴァイテル フランツ
    共同の研究課題数: 3件
    共同の研究成果数: 10件
  • 9.  廣川 佐千男 (40126785)
    共同の研究課題数: 2件
    共同の研究成果数: 0件
  • 10.  田栗 正章 (10009607)
    共同の研究課題数: 2件
    共同の研究成果数: 0件
  • 11.  今野 良彦 (00205577)
    共同の研究課題数: 2件
    共同の研究成果数: 0件
  • 12.  中神 潤一 (30092076)
    共同の研究課題数: 2件
    共同の研究成果数: 0件
  • 13.  藤田 憲悦 (30228994)
    共同の研究課題数: 2件
    共同の研究成果数: 0件
  • 14.  ポッター リチャード
    共同の研究課題数: 2件
    共同の研究成果数: 5件
  • 15.  レオンワタナキット ワチャリン
    共同の研究課題数: 2件
    共同の研究成果数: 5件
  • 16.  セビ ナジム
    共同の研究課題数: 2件
    共同の研究成果数: 0件
  • 17.  横山 重俊 (10600968)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 18.  種村 秀紀 (40217162)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 19.  橋本 明浩 (60164779)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 20.  宮埜 壽夫 (90200196)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 21.  金沢 誠 (20261886)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 22.  玉井 哲雄 (60217172)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 23.  白石 高章 (50143160)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 24.  滝澤 由美 (90280528)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 25.  鹿島 亮 (10240756)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 26.  山形 頼之 (40415758)
    共同の研究課題数: 1件
    共同の研究成果数: 3件
  • 27.  渚 勝 (50189172)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 28.  中村 吉邑 (90110270)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 29.  西崎 真也 (90263615)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 30.  腰越 秀之 (70110294)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 31.  中神 祥臣 (70091246)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 32.  峰村 勝弘 (20060684)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 33.  安田 正実 (00041244)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 34.  多田 充 (20303331)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 35.  湯浅 能史
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 36.  逸見 港
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 37.  コハン アレクサンダー
    共同の研究課題数: 1件
    共同の研究成果数: 2件
  • 38.  馬 雷
    共同の研究課題数: 1件
    共同の研究成果数: 4件

URL: 

この研究者とORCID iDの連携を行いますか?
※ この処理は、研究者本人だけが実行できます。

Are you sure that you want to link your ORCID iD to your KAKEN Researcher profile?
* This action can be performed only by the researcher himself/herself who is listed on the KAKEN Researcher’s page. Are you sure that this KAKEN Researcher’s page is your page?

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi