対話的定理証明によるソフトウェアの精密な検証

2008 年度 研究成果報告書

• 研究課題/領域番号: 18700018
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 筑波大学
• 研究代表者: 南出 靖彦 筑波大学, 大学院・システム情報工学研究科, 准教授 (50252531)
• 研究期間 (年度): 2006 – 2008
• キーワード: ソフトウェア検証 / 定理証明系 / ホーア論理

研究概要

対話的定理証明によるソフトウェアの検証について、様々な角度から研究を行い、事例研究を通じ、小規模なソフトウェアやソフトウェアの核となる部分については、対話的定理証明による検証が可能であることを示した。特に、本研究の代表者が開発しているウェブプログラムの検証ツールPHP文字列解析器について、その核となるアルゴリズムの定式化・検証を行い、正当性を検証済みのプログラムを得ることに成功した。

研究成果

• [雑誌論文] Copy-on-Write in the PHP Language (2009)
  • 著者名/発表者名: A. Tozawa, M. Tatsubori, T. Onodera, Y. Minamide
  • 雑誌名: InProc. POPL : The Symposium on Principles of Programming Languages ページ: 200-212
  • 査読あり
• [雑誌論文] Approximation of String Operations in the PHP String Analyzer (2008)
  • 著者名/発表者名: Y. Minamide
  • 雑誌名: Proc. of Symbolic Computation in Software Science Austrian-Japanese Workshop, RISC Technical Report 08-08 ページ: 137-147
• [雑誌論文] A Translation from the HTML DTD into a Regular Hedge Grammar (2008)
  • 著者名/発表者名: T. Nishiyama, Y. Minamide
  • 雑誌名: In Proc. of the 13th International Conference on Implementation and Application of Automata LNCS 5148 ページ: 122-131
  • 査読あり
• [雑誌論文] 多相レコード型に基づくRubyプログラムの型推論 (2008)
  • 著者名/発表者名: 松本宗太郎, 南出靖彦
  • 雑誌名: 情報処理学会論文誌 : プログラミング Vol.49, No.SIG 3, PRO 36 ページ: 39-54
  • 査読あり
• [雑誌論文] ソフトウェア解説 : Cプログラムの検証ツール Caduceus (2007)
  • 著者名/発表者名: 南出靖彦
  • 雑誌名: コンピュータソフトウェア Vol.24, No.3 ページ: 15-19
  • 査読あり
• [雑誌論文] Verified Decision Procedures on Context-Free Grammars (2007)
  • 著者名/発表者名: Y.Minamide
  • 雑誌名: In Proc. of the 20th International Conference on Theorem Proving in Higher Order Logics LNCS 4732 ページ: 173-188
  • 査読あり
• [雑誌論文] Complexity Results on Balanced Context-Free Languages (2007)
  • 著者名/発表者名: A.Tozawa, Y. Minamide
  • 雑誌名: In Proc. of the Tenth International Conference on Foundations of Software Science and Computation Structures LNCS 4423 ページ: 346-3601
  • 査読あり
• [雑誌論文] XML Validation for Context-Free Grammars (2006)
  • 著者名/発表者名: Y. Minamide, A. Tozawa
  • 雑誌名: In Proceedings of the Fourth Asian Symposium on Programming Languages and Systems (APLAS) LNCS 4279 ページ: 357-373
  • 査読あり
• [学会発表] ブラウザにおけるJavaScript 実行のモデル化 (2008)
  • 著者名/発表者名: 安田峰悠, 松本宗太郎, 南出靖彦
  • 学会等名: 日本ソフトウェア科学会第25回大会
  • 発表場所: 筑波大学東京キャンパス
  • 年月日: 2008-09-10
• [学会発表] 動的に生成されるHTML文書の妥当性検査 (2008)
  • 著者名/発表者名: 西山拓哉, 南出靖彦
  • 学会等名: 日本ソフトウェア科学会第25回大会
  • 発表場所: 筑波大学東京キャンパス
  • 年月日: 2008-09-10
• [学会発表] 多相型レコードに基づくRubyオブジェクトの型推論に関する考察 (2006)
  • 著者名/発表者名: 松本宗太郎, 南出靖彦
  • 学会等名: 日本ソフトウェア科学会第23回大会
  • 発表場所: 東京大学
  • 年月日: 2006-09-15
• [備考]
  • URL: http://www.score.cs.tsukuba.ac.jp/~minamide/verification.html