• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Verification of Software with Interactive Theorem Proving

Research Project

Project/Area Number 18700018
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Software
Research InstitutionUniversity of Tsukuba

Principal Investigator

MINAMIDE Yasuhiko  University of Tsukuba, 大学院・システム情報工学研究科, 准教授 (50252531)

Project Period (FY) 2006 – 2008
Project Status Completed (Fiscal Year 2008)
Budget Amount *help
¥3,400,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥300,000)
Fiscal Year 2008: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2007: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2006: ¥1,100,000 (Direct Cost: ¥1,100,000)
Keywordsソフトウェア検証 / 定理証明系 / ホーア論理 / Hoare論理 / 対話的定理証明 / プログラム解析
Research Abstract

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

Report

(4 results)
  • 2008 Annual Research Report   Final Research Report ( PDF )
  • 2007 Annual Research Report
  • 2006 Annual Research Report
  • Research Products

    (20 results)

All 2009 2008 2007 2006 Other

All Journal Article (15 results) (of which Peer Reviewed: 12 results) Presentation (4 results) Remarks (1 results)

  • [Journal Article] Copy-on-Write in the PHP Language2009

    • Author(s)
      A. Tozawa, M. Tatsubori, T. Onodera, Y. Minamide
    • Journal Title

      InProc. POPL : The Symposium on Principles of Programming Languages

      Pages: 200-212

    • Related Report
      2008 Final Research Report
    • Peer Reviewed
  • [Journal Article] Copy-on-Write in the PHP Language2009

    • Author(s)
      A. Tozawa, M. Tatsubori, T. Onodera, Y. Minamide
    • Journal Title

      Proc. POPL : The Symposium on Principle s of Programming Languages

      Pages: 200-212

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Approximation of String Operations in the PHP String Analyzer2008

    • Author(s)
      Y. Minamide
    • Journal Title

      Proc. of Symbolic Computation in Software Science Austrian-Japanese Workshop, RISC Technical Report 08-08

      Pages: 137-147

    • Related Report
      2008 Final Research Report
  • [Journal Article] A Translation from the HTML DTD into a Regular Hedge Grammar2008

    • Author(s)
      T. Nishiyama, Y. Minamide
    • Journal Title

      In Proc. of the 13th International Conference on Implementation and Application of Automata LNCS 5148

      Pages: 122-131

    • Related Report
      2008 Final Research Report
    • Peer Reviewed
  • [Journal Article] 多相レコード型に基づくRubyプログラムの型推論2008

    • Author(s)
      松本宗太郎, 南出靖彦
    • Journal Title

      情報処理学会論文誌 : プログラミング Vol.49, No.SIG 3, PRO 36

      Pages: 39-54

    • NAID

      110006684629

    • Related Report
      2008 Final Research Report
    • Peer Reviewed
  • [Journal Article] A Translation from the HTML DTD into a Regular Hedge Grammar2008

    • Author(s)
      T. Nishiyama, Y. Minamide
    • Journal Title

      Proc. of the 13th International Confer ence on Implementation and Application of Automata LNCS5148

      Pages: 122-131

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 多相レコード型に基づくRubyプログラムの型推論2008

    • Author(s)
      松本, 宗太郎・南出, 靖彦
    • Journal Title

      情報処理学会論文誌:プログラミング 49

      Pages: 39-54

    • NAID

      110006684629

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] ソフトウェア解説 : Cプログラムの検証ツール Caduceus2007

    • Author(s)
      南出靖彦
    • Journal Title

      コンピュータソフトウェア Vol.24, No.3

      Pages: 15-19

    • Related Report
      2008 Final Research Report
    • Peer Reviewed
  • [Journal Article] Verified Decision Procedures on Context-Free Grammars2007

    • Author(s)
      Y.Minamide
    • Journal Title

      In Proc. of the 20th International Conference on Theorem Proving in Higher Order Logics LNCS 4732

      Pages: 173-188

    • Related Report
      2008 Final Research Report
    • Peer Reviewed
  • [Journal Article] Complexity Results on Balanced Context-Free Languages2007

    • Author(s)
      A.Tozawa, Y. Minamide
    • Journal Title

      In Proc. of the Tenth International Conference on Foundations of Software Science and Computation Structures LNCS 4423

      Pages: 346-3601

    • Related Report
      2008 Final Research Report
    • Peer Reviewed
  • [Journal Article] Verified Decision Procedures on Context-Free Grammars2007

    • Author(s)
      Yasuhiko, Minamide
    • Journal Title

      International Conference on Theorem Proving in Higher Order Logics LNCS 4732

      Pages: 173-188

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Cプログラムの検証ツール Caduceus2007

    • Author(s)
      南出, 靖彦
    • Journal Title

      コンピュータコンピュータソフトウェア 24

      Pages: 15-19

    • NAID

      130004549074

    • Related Report
      2007 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Complexity Results on Balanced Context-Free Languages2007

    • Author(s)
      Akihiko Tozawa, Yasuhiko Minamide
    • Journal Title

      Tenth International Conference on Foundations of Software Science and Computation Structures LNCS 4423

      Pages: 346-360

    • Related Report
      2006 Annual Research Report
  • [Journal Article] XML Validation for Context-Free Grammars2006

    • Author(s)
      Y. Minamide, A. Tozawa
    • Journal Title

      In Proceedings of the Fourth Asian Symposium on Programming Languages and Systems (APLAS) LNCS 4279

      Pages: 357-373

    • Related Report
      2008 Final Research Report
    • Peer Reviewed
  • [Journal Article] XML Validation for Context-Free Grammars2006

    • Author(s)
      Yasuhiko Minamide, Akihiko Tozawa
    • Journal Title

      Fourth ASIAN Symposium on Programming Languages and Systems LNCS 4279

      Pages: 357-373

    • Related Report
      2006 Annual Research Report
  • [Presentation] ブラウザにおけるJavaScript 実行のモデル化2008

    • Author(s)
      安田峰悠, 松本宗太郎, 南出靖彦
    • Organizer
      日本ソフトウェア科学会第25回大会
    • Place of Presentation
      筑波大学東京キャンパス
    • Year and Date
      2008-09-10
    • Related Report
      2008 Final Research Report
  • [Presentation] 動的に生成されるHTML文書の妥当性検査2008

    • Author(s)
      西山拓哉, 南出靖彦
    • Organizer
      日本ソフトウェア科学会第25回大会
    • Place of Presentation
      筑波大学東京キャンパス
    • Year and Date
      2008-09-10
    • Related Report
      2008 Annual Research Report 2008 Final Research Report
  • [Presentation] ブラウザにおけるJavaScript実行のモデル化2008

    • Author(s)
      安田峰悠, 松本宗太郎, 南出靖彦
    • Organizer
      日本ソフトウェア科学会第25回大会
    • Place of Presentation
      筑波大学東京キャンパス
    • Year and Date
      2008-09-10
    • Related Report
      2008 Annual Research Report
  • [Presentation] 多相型レコードに基づくRubyオブジェクトの型推論に関する考察2006

    • Author(s)
      松本宗太郎, 南出靖彦
    • Organizer
      日本ソフトウェア科学会第23回大会
    • Place of Presentation
      東京大学
    • Year and Date
      2006-09-15
    • Related Report
      2008 Final Research Report
  • [Remarks]

    • URL

      http://www.score.cs.tsukuba.ac.jp/~minamide/verification.html

    • Related Report
      2008 Final Research Report

URL: 

Published: 2006-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi