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

Modeling and verification of web software based on theories symbolic computation

Research Project

Project/Area Number 20300001
Research Category

Grant-in-Aid for Scientific Research (B)

Allocation TypeSingle-year Grants
Section一般
Research Field Fundamental theory of informatics
Research InstitutionUniversity of Tsukuba

Principal Investigator

IDA Tetsuo  筑波大学, システム情報系, 教授 (70100047)

Co-Investigator(Kenkyū-buntansha) MINAMIDE Yasuhiko  筑波大学, システム情報系, 准教授 (50252531)
MARIN Mircea  筑波大学, システム情報系, 講師 (60396603)
SUSUKI Taro  会津大学, コンピュータ理工学部, 准教授 (90272179)
Project Period (FY) 2008 – 2011
Project Status Completed (Fiscal Year 2011)
Budget Amount *help
¥19,110,000 (Direct Cost: ¥14,700,000、Indirect Cost: ¥4,410,000)
Fiscal Year 2011: ¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2010: ¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2009: ¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2008: ¥7,150,000 (Direct Cost: ¥5,500,000、Indirect Cost: ¥1,650,000)
Keywordsソフトウェア検証 / 記号計算 / ウェブ / 情報基礎 / ソフトウェア / 検証 / ソフトウェア学
Research Abstract

As a case study of Web software verification, we have verified the core of WebEos. The effective verification was conducted by utilizing some results of the computation conducted on Mathematica. With respect to the verification based on string analysis, we developed the method to precisely analyze regular expression matching. By introducing the analysis of communication to database, we enabled the detection of stored XSS. We designed and implemented an algorithm of greedy regular expression matching based on position automata.

Report

(6 results)
  • 2011 Annual Research Report   Final Research Report ( PDF )
  • 2010 Annual Research Report   Self-evaluation Report ( PDF )
  • 2009 Annual Research Report
  • 2008 Annual Research Report
  • Research Products

    (47 results)

All 2012 2011 2010 2009 2008

All Journal Article (32 results) (of which Peer Reviewed: 31 results) Presentation (15 results)

  • [Journal Article] Translating Regular Expression Matching into Transducers2012

    • Author(s)
      Yuto Sakuma, Yasuhiko Minamide, Andrei Voronkov
    • Journal Title

      Journal of Applied Logic

      Volume: 10 Pages: 32-51

    • Related Report
      2011 Annual Research Report 2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Design and Implementation of New Generation Data Format for Lunar and Planetary Exploration2012

    • Author(s)
      Taro SUZUKI, Junya TERAZONO, Takafumi HAYASHI
    • Journal Title

      JSASS on-line journal Aerospace Technology

    • NAID

      130003373361

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Design and Implementation of New Generation Data Format for Lunar and Planetary Exploration2012

    • Author(s)
      Taro SUZUKI, Junya TERAZONO, Takafumi HAYASHI
    • Journal Title

      JSASS on-line journal "Aerospace Technology"

      Volume: (to appear)

    • NAID

      130003373361

    • Related Report
      2011 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Morley's theorem revisited : Origami construction and automated proof2011

    • Author(s)
      Ida. T, Kasem. A, Ghourabi. F, Takahashi. H
    • Journal Title

      Journal of Symbolic Computation

      Volume: vol. 46 Pages: 162-170

    • NAID

      120007130912

    • Related Report
      2011 Final Research Report 2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Proof Assistant Decision Procedures for Formalizing Origami2011

    • Author(s)
      Kaliszyk. C, and Ida. T
    • Journal Title

      Lecture Notes in Computer Science (proceedings of the Conference on Intelligent Computer Mathematics (CICM' 11))

      Volume: 6824 Pages: 45-57

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Proof Documents for Automated Origami Theorem Proving2011

    • Author(s)
      Ghourabi. F, Ida. T, and Kasem. A
    • Journal Title

      Lecture Notes in Computer Science (post-proceeding of the 8th International Workshop on Automated Deduction in Geometry (ADG 2010))

      Volume: 6877 Pages: 78-97

    • Related Report
      2011 Annual Research Report 2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Origami Axioms and Circle Extension2011

    • Author(s)
      Kasem. A, Ghourabi. F, Ida. T
    • Journal Title

      Proceedings of the 26th Symposium on Applied Computing (SAC 2011)

      Pages: 1106-1111

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Proof Assistant Decision Procedures for Formalizing Origami2011

    • Author(s)
      Kaliszyk. C, Ida. T
    • Journal Title

      Lecture Notes in Computer Science (proceedings of the Conference on Intelligent Computer Mathematics (CICM'11))

      Volume: 6824 Pages: 45-57

    • DOI

      10.1007/978-3-642-22673-1_4

    • ISBN
      9783642226724, 9783642226731
    • Related Report
      2011 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Morley's theorem revisited : Origami construction and automated proof2011

    • Author(s)
      Ida.T, Kasem.A, Ghourabi.F, Takahashi.H
    • Journal Title

      Journal of Symbolic Computation vol.46

      Pages: 162-170

    • NAID

      120007130912

    • Related Report
      2010 Self-evaluation Report
    • Peer Reviewed
  • [Journal Article] Disambiguation in Regular Expression Matching via Position Automata with Augmented Transitions2011

    • Author(s)
      Satoshi Okui, Taro Suzuki
    • Journal Title

      Lecture Notes in Computer Science

      Volume: 6482 Pages: 231-240

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Translating Regular Expression Matching into Transducers2011

    • Author(s)
      Yasuhiko Minamide, Yuto Sakuma, Andrei Voronkov
    • Journal Title

      Proc.International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2010)

      Pages: 107-115

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Origami Fold as Algebraic Graph Rewriting2010

    • Author(s)
      Tetsuo Ida and Hidekazu Takahashi
    • Journal Title

      Journal of Symbolic Computation

      Volume: 45(4) Pages: 393-413

    • NAID

      120007138181

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Rubyプログラムの制御フロー解析とその健全性の証明2010

    • Author(s)
      松本宗太郎, 南出靖彦
    • Volume
      3巻
    • Pages
      9-25
    • NAID

      110007970972

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Origami Fold as Algebraic Graph Rewriting.2010

    • Author(s)
      Tetsuo Ida, Hidekazu Takahashi
    • Journal Title

      Journal of Symboli Computation 45(4)

      Pages: 393-413

    • NAID

      120007138181

    • Related Report
      2010 Self-evaluation Report
  • [Journal Article]2010

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

      Rubyプログラムの制御フロー解析とその健全性の証明 3巻

      Pages: 9-25

    • Related Report
      2010 Self-evaluation Report
    • Peer Reviewed
  • [Journal Article] Rubyプログラムの制御フロー解析とその健全性の証明2010

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

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

      Pages: 9-25

    • NAID

      110007970972

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Linear Systems for Regular Hedge Languages2010

    • Author(s)
      Mircea Marin, Temur Kutsia
    • Journal Title

      Advances in Databases and Information Systems. Associated Workshops and Doctoral Consortium of ADBIS 2009. Proceedings. LNCS 5968

      Pages: 104-112

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Copy-on-Write in the PHP Langauge2009

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

      Proc. of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

      Pages: 200-212

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Symbolic and Algebraic Methods in Computational Origami : Invited Talk2009

    • Author(s)
      Tetsuo Ida
    • Journal Title

      In Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation (ISSAC 2009)

      Pages: 3-4

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Origami Fold as Algebraic Graph Rewriting2009

    • Author(s)
      Tetsuo Ida, Hidekaza Takahashi
    • Journal Title

      Proc. of 24th annual ACM Symposium on Applied Computing

      Pages: 1132-1138

    • NAID

      120007138181

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Graph Rewriting in Computational Origami2009

    • Author(s)
      Ida, T
    • Journal Title

      Proceedings of the 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing(SYNASC 2008)

      Pages: 20-27

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Theorem Proving Based on the Characteristic Set Method for Computational Origami Constructions2009

    • Author(s)
      Ghourabi, F, Ida, T, Wang, D
    • Journal Title

      Proceedings of the Tunisia-Japan Workshop on Symbolic Computation in Software Science(SCSS 2009)

      Pages: 90-92

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Hedge Pattern Partial Derivative2009

    • Author(s)
      T.Suzuki, S.Okui
    • Journal Title

      14-th International Conference on Implementation and Application of Automata(CIAA 2009), Lecture Notes in Computer Science 5642

      Pages: 125-134

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Origami Fold as Algebraic Graph Rewriting2009

    • Author(s)
      Tetsuo Ida, Hidekazu Takahas hi
    • Journal Title

      24th annual ACM, Symposium on Applied Computing (SAC 2009)

      Pages: 1132-1138

    • NAID

      120007138181

    • Related Report
      2008 Annual 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 Principles of Programming Languages

      Pages: 200-212

    • Related Report
      2008 Annual 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 13th International Conference on Implementation and Application of Automata

      Pages: 122-131

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Product Drivatives of Regular Expressions2008

    • Author(s)
      Taro Suzuki, Staoshi Okui
    • Journal Title

      IPSJ Online Transactions

      Volume: 1巻 Pages: 53-65

    • Related Report
      2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] Product Drivatives of Regular Expressions2008

    • Author(s)
      Taro Suzuki, Staoshi Okui
    • Journal Title

      IPSJ Online Transactions 1巻

      Pages: 53-65

    • Related Report
      2010 Self-evaluation Report
    • Peer Reviewed
  • [Journal Article] WEBEOS: A System for Origami Construction and Proving on the Web2008

    • Author(s)
      Tetsuo Ida, Asem Kasem
    • Journal Title

      The INTERNATIONAL INSTITUTE for ADVANCED STUDIES in SYSTEMS RESEARCH and CYBERNETICS 2

      Pages: 53-59

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Computational Origami Construction as Colistraint Solving and Rewriting2008

    • Author(s)
      Tetsuo Ida, Mircea Marin, Hidekazu Takahashi, Fadoua Ghourabi
    • Journal Title

      Electronic Notes in Theoretical Computer Science 216

      Pages: 31-44

    • Related Report
      2008 Annual 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 Conference on-Implementation and Application of Automata LNCS 5184

      Pages: 122-131

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Product Derivatives of Regular Expressions2008

    • Author(s)
      Taro Suzuki, Satoshi Okui
    • Journal Title

      IPSJ Online Transactions 1

      Pages: 53-65

    • NAID

      130000022133

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Presentation] 文字列解析によるクロスサイトスクリプティング脆弱性検査の改良2012

    • Author(s)
      木村将人, 南出靖彦
    • Organizer
      プログラミングおよびプログラミング言語ワークショップ(ポスター)
    • Place of Presentation
      和歌山県南紀白浜
    • Year and Date
      2012-03-08
    • Related Report
      2011 Final Research Report
  • [Presentation] Origami Axioms and Circle Extension2011

    • Author(s)
      Kasem.A, Ghourabi.F, Ida.T
    • Organizer
      Proceedings of the 26th Symposium on Applied Computing (SAC 2011), pp.1106-1111
    • Place of Presentation
      Tunghai University Taiwan
    • Year and Date
      2011-03-23
    • Related Report
      2010 Self-evaluation Report
  • [Presentation] Extended Web Services for Computational Origami. The 3rd International Workshop on Symbolic Computation in Software Science (SCSS2010)2010

    • Author(s)
      Kasem and T. Ida
    • Organizer
      RISC-Linz Report Series
    • Place of Presentation
      Hagenberg, Austria
    • Year and Date
      2010-07-30
    • Related Report
      2011 Final Research Report
  • [Presentation] バックトラックのないマッチングオートマトンを用いたXML変換のためのアルゴリズム2010

    • Author(s)
      柴田裕哉, 鈴木大郎
    • Organizer
      第78回情報処理学会プログラミング研究会
    • Place of Presentation
      電気通信大学
    • Year and Date
      2010-03-16
    • Related Report
      2009 Annual Research Report
  • [Presentation] Rubyのコア言語の操作的意味論2009

    • Author(s)
      松本宗太郎, 南出靖彦
    • Organizer
      日本ソフトウェア科学会第26回大会
    • Place of Presentation
      島根大学
    • Year and Date
      2009-09-16
    • Related Report
      2011 Final Research Report
  • [Presentation] Copy-on-Write in the PHP Langauge2009

    • Author(s)
      Tozawa, M.Tatsubori, T.Onodera, Y.Minamide
    • Organizer
      Proc.of the 13^<th> International Conference on Programming Languages, pp.200-212
    • Place of Presentation
      Lyon, France
    • Year and Date
      2009-08-23
    • Related Report
      2010 Self-evaluation Report
  • [Presentation] Reasoning Tool for Mathematical Origami Construction2009

    • Author(s)
      F. Ghourabi, T. Ida, H. Takahashi, and A. Kasem
    • Organizer
      The International Symposium on Symbolic and Algebraic Computation (ISSAC 2009)
    • Place of Presentation
      Seoul, Korea
    • Year and Date
      2009-07-30
    • Related Report
      2011 Final Research Report
  • [Presentation] Reasoning Tool for Mathematical Origami Construction2009

    • Author(s)
      Ghourabi, F, Ida, T, Takahashi, H, Kasem, A
    • Organizer
      ISSAC09 Software Presentation. ACM
    • Place of Presentation
      KIAS(Korea Institute for Advanced study)
    • Year and Date
      2009-07-30
    • Related Report
      2009 Annual Research Report
  • [Presentation] Origami Fold as Algebraic Graph Rewriting2009

    • Author(s)
      Tetsuo Ida, Hidekaza Takahashi
    • Organizer
      Proc.of 24^<th> annual ACM Symposium on Applied Computing, pp.1132-1138
    • Place of Presentation
      Hawaii, USA
    • Year and Date
      2009-03-12
    • Related Report
      2010 Self-evaluation Report
  • [Presentation] Symbolic and Algebraic Methods in Computational Origami : Invited Talk.2009

    • Author(s)
      Tetsuo Ida.
    • Organizer
      In Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation (ISSAC 2009), pages 3-4. ACM
    • Place of Presentation
      Hawaii, USA.
    • Related Report
      2010 Self-evaluation Report
  • [Presentation] Experiences with Web Environment Origamium2008

    • Author(s)
      Kasem and T. Ida
    • Organizer
      日本ソフトウェア科学会第25回大会
    • Place of Presentation
      筑波大学(東京キャンパス)
    • Year and Date
      2008-09-11
    • Related Report
      2011 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] 動的に生成されるHTML文書の妥当性検査2008

    • Author(s)
      西山拓哉,南出靖彦
    • Organizer
      日本ソフトウェア科学会第25回大会
    • Place of Presentation
      筑波大学(東京キャンパス)
    • Year and Date
      2008-09-10
    • Related Report
      2008 Annual Research Report
  • [Presentation] A Translation from the HTML DTD into a Regular Hedge Grammar2008

    • Author(s)
      T.Nishiyama, Y.Minamide
    • Organizer
      Proc.of 13^<th> International Conference on Implementation and Application of Automata, pp.122-131
    • Place of Presentation
      California, USA
    • Year and Date
      2008-07-21
    • Related Report
      2010 Self-evaluation Report
  • [Presentation] Experiences with Web Environment Origamium: Examples and Applications2008

    • Author(s)
      Asem Kasem, Tetsuo Ida
    • Organizer
      Austrian-japanese Workshop on Symbolic Complutation in Software Science (SCSS 2008)
    • Place of Presentation
      RISC, Hagenberg, Austria
    • Year and Date
      2008-07-13
    • Related Report
      2008 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi