様相論理の決定手続きとソフトウェア検証への応用

• 研究課題/領域番号: 21500006
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 情報学基礎
• 研究機関: 国立情報学研究所 (2010-2011); 東京大学 (2009)
• 研究代表者: 田辺 良則 国立情報学研究所, アーキテクチャ科学研究系, 特任研究員 (60443199)
• 研究期間 (年度): 2009 – 2011
• 研究課題ステータス: 完了 (2011年度)
• 配分額: 2,730千円 (直接経費: 2,100千円、間接経費: 630千円); 2011年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2010年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2009年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
• キーワード: 様相論理 / 決定手続き / ソフトウェア検証 / モデル検査 / 充足可能性 / 様相μ計算 / min-plus代数 / 法定手続き

研究概要

様相論理を用いたポインタ操作プログラムの検証,特に停止性判定への応用を図るために必要な理論を構築した.ひとつには,クリプキ構造操作に対する最弱事前条件および最強事後条件の解明であり,もう一つは様相μ計算の意味論の拡張である.後者では,真偽値がmin-plus代数N∞に値をとるような体系を構築し,この体系上でのモデル検査問題と充足可能性判定問題に解を与えた.

研究成果

• [雑誌論文] Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications (2011)
  • 著者名/発表者名: Kosuke Ono, Yoichi Hirai, Masami Hagiya and Yoshinori Tanabe
  • 雑誌名: Proceedings of 9th International Conference on Software Engineering and Formal Methods(SEFM 2011) 巻: Vol.7041 ページ: 350-365
  • 査読あり
• [雑誌論文] Model Checking Distributed Systems by Combining Caching and Process Checkpointing (2011)
  • 著者名/発表者名: Watcharin Leungwattanakit, Cyrille Artho, Masami Hagiya, Yoshinori Tanabe, and Mitsuharu Yamamoto
  • 雑誌名: Proceedings of 26th IEEE/ACM International Conference on Automated Software Engineering(ASE) ページ: 103-112
  • 査読あり
• [雑誌論文] Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications (2011)
  • 著者名/発表者名: Kosuke Ono, Yoichi Hirai, Masami Hagiya Natsuko Noda
  • 雑誌名: Lecture Notes in Computer Science 巻: 7041 ページ: 350-365
  • DOI: 10.1007/978-3-642-24690-6_24
  • ISBN: 9783642246890, 9783642246906
  • 査読あり
• [雑誌論文] Model checking distributed systems by combining caching and process checkpointing (2011)
  • 著者名/発表者名: Watcharin Leungwattanakit
  • 雑誌名: 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) 巻: 1 ページ: 103-112
  • DOI: 10.1109/ase.2011.6100043
  • 査読あり
• [雑誌論文] Decidability and Undecidability Results of Modalμ-calculi with N-infinity Semantics (2010)
  • 著者名/発表者名: Alexis Goyet, Masami Hagiya, Yoshinori Tanabe
  • 雑誌名: Proceedings of 17th Internaional Workshop of Logic, Language, Information and Computation(WoLLIC2010) ページ: 148-160
  • 査読あり
• [雑誌論文] Modalμ-calculus on min-plus algebra N-infinity (2010)
  • 著者名/発表者名: Dai Ikarashi, Yoshinori Tanabe, Koki Nishizawa, Masami Hagiya
  • 雑誌名: コンピュータソフトウェア 巻: Vol.27, No.3 ページ: 99-113
  • 査読あり
• [雑誌論文] Decidability and Undecidability Results of Modal μ-calculi with N-infinity Semantics (2010)
  • 著者名/発表者名: Alexis Goyet, Masami Hagiya, Yoshinori Tanabe
  • 雑誌名: WOLLIC2010, Lecture Notes in Artificial Intelligence 巻: 6188 ページ: 148-160
  • 査読あり
• [雑誌論文] Fixed-point Computations over Functions on Integers with Operations Min, Max and Plus (2009)
  • 著者名/発表者名: Masami Hagiya, Yoshinori Tanabe
  • 雑誌名: Proceedings of 6th Workshop on Fixed Points in Computer Science(FICS2009) ページ: 108-115
  • 査読あり
• [雑誌論文] Pre-and Post-conditions Expressed in Variants of the Modalμ-calculus (2009)
  • 著者名/発表者名: Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, Koichi Takahashi
  • 雑誌名: IEICE Transactions on Information and Systems 巻: Vol.E92-D ページ: 995-1002
  • NAID: 10026809282
  • 査読あり
• [雑誌論文] Pre- and Post-conditions Expressed in Variants of the Modal μ-calculus (2009)
  • 著者名/発表者名: Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, Koichi Takahashi
  • 雑誌名: IEICE Transactions on Information and Systems Vol.E92-D ページ: 995-1002
  • NAID: 10026809282
  • 査読あり
• [学会発表] ネットワークアプリケーションのマスター・スレーブ方式モデル検査アルゴリズムについて (2012)
  • 著者名/発表者名: 田辺良則, Cyriile Artho, Watcharin Leungwattanakit,山本光晴,萩谷昌己
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 沖縄産業支援センター
  • 年月日: 2012-09-29
• [学会発表] Coqを使用したMap Reduceアプリケーションの検証とScalaコードの抽出 (2012)
  • 著者名/発表者名: 姜帆,田辺良則,本位田真一
  • 学会等名: 第14回プログラミングおよびプログラミング言語ワークショップ(PPL2012)
  • 発表場所: 和歌山県白浜町旅館むさし
  • 年月日: 2012-03-09
• [学会発表] Coqを使用したMapReduceアプリケーションの検証とScalaコードの抽出 (2012)
  • 著者名/発表者名: 姜帆
  • 学会等名: 第14回プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 和歌山県南紀白浜むさし
  • 年月日: 2012-03-09
• [学会発表] ネットワークアプリケーションのマスター・スレーブ方式モデル検査アルゴリズムについて (2011)
  • 著者名/発表者名: 田辺良則
  • 学会等名: 日本ソフトウェア科学会第28回大会
  • 発表場所: 沖縄産業支援センター
  • 年月日: 2011-09-28
• [学会発表] Toward Liveness Verification in Java Pathfinder (2009)
  • 著者名/発表者名: Yoshinori Tanabe, Vinh Cuong Tran, Masami Hagiya
  • 学会等名: 第6回ディペンダブルシステムシンポジウム(dss2009)
  • 発表場所: 大阪大学大学院
  • 年月日: 2009-12-14
• [学会発表] Games and Natural Number-valued Semantics of the Modalμ-calculus (2009)
  • 著者名/発表者名: Masami Hagiya, Yoshinori Tanabe
  • 学会等名: 日本ソフトウェア科学会第26回大会
  • 発表場所: 島根大学
  • 年月日: 2009-09-16
• [学会発表] Games and Natural Number-valued Semantics of the Modal μ-calculus (2009)
  • 著者名/発表者名: Masami Hagiya, Yoshinori Tanabe(登壇)
  • 学会等名: 日本ソフトウェア科学会第26回大会
  • 発表場所: 島根大学
  • 年月日: 2009-09-16
• [学会発表] Fixed-point Computations over Functions on Integers with Operations Min, Max and Plus (2009)
  • 著者名/発表者名: Masami Hagiya, Yoshinori Tanabe(登壇)
  • 学会等名: 6th Workshop on Fixed Points in Computer Science (FICS 2009)
  • 発表場所: University of Coimbra, Portugal
  • 年月日: 2009-09-13
• [学会発表] Decidability and Undecidability Results of Modalμ-calculi with N-infinity Semantics (2009)
  • 著者名/発表者名: Alexis Goyet, Masami Hagiya, Yoshinori Tanabe
  • 学会等名: 情報処理学会プログラミング研究会(PRO)
  • 発表場所: 東京工業大学
  • 年月日: 2009-06-08
• [学会発表] Decidability and Undecidability Results of Modal μ-calculi with N-infinity Semantics (2009)
  • 著者名/発表者名: Alexis Goyet, Masami Hagiya, Yoshinori Tanabe(登壇)
  • 学会等名: 情報処理学会プログラミング研究会(PRO)
  • 発表場所: 東京工業大学
  • 年月日: 2009-06-08