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

2018 年度 実績報告書

形式言語理論を駆使したウェブ基盤技術の検証

研究課題

研究課題/領域番号 15K00087
研究機関東京工業大学

研究代表者

南出 靖彦  東京工業大学, 情報理工学院, 教授 (50252531)

研究期間 (年度) 2015-04-01 – 2019-03-31
キーワードソフトウェア検証 / 形式言語理論 / ウェブ / 正規表現
研究実績の概要

ウェブ基盤技術の検証のための基礎理論として以下の研究を行った.
1)Streaming Transducerのコピーに関する制限を緩和したBounded Streaming Transducerに関する研究を行い,合成の具体的構成を与えた.さらに,証明支援系Isabelle/HOLによりBounded Streaming Transducerの形式化を行い,合成の構成の正しさを証明した.
2)ウェブプログラム検証の基盤技術となる文字列制約の充足可能性判定の研究を行った.直線形式(straight-line form)と呼ばれる制限された形式の制約について,Streaming Transducer を用いた充足可能性判定手続きを開発し,プロトタイプ実装を行なった.この充足可能性判定において,Streaming Transducerの合成が重要な役割を果たす.また,Bounded Streaming Trasnducer を用いることで,判定手続きの自然な形式化および実装が可能となっている.
3)先読み付き正規表現に対して微分を導入し,先読み付き正規表現からオートマトンへの変換を与えた.さらに,この変換を精密に分析することで,先読み付き正規表現からオートマトンへの変換の状態数に関する2重指数の上界を与えた.
4)バックトラックによる正規表現マッチングの計算量解析に関して,効率的な判定器を実装する研究を行った.WeberとSeidlによるオートマトンの曖昧度の判定アルゴリズムの手法と本研究で開発してきた文字列から木へのトランスデューサに基づく手法を組み合わせることで効率的な判例アルゴリズムを構築した.これまでの実装でタイムアウトになっていた正規表現についても実用的な時間内での判定が可能となった.

  • 研究成果

    (4件)

すべて 2019 2018

すべて 雑誌論文 (1件) (うち査読あり 1件、 オープンアクセス 1件) 学会発表 (3件)

  • [雑誌論文] Derivatives of Regular Expressions with Lookahead2019

    • 著者名/発表者名
      Takayuki Miyazaki, Yasuhiko Minamide
    • 雑誌名

      Journal of Information Processing

      巻: 未定 ページ: 9ページ

    • 査読あり / オープンアクセス
  • [学会発表] 先読み付き正規表現の微分2018

    • 著者名/発表者名
      宮嵜 貴之, 南出 靖彦
    • 学会等名
      情報処理学会プログラミング研究会 第121回プログラミング研究発表会
  • [学会発表] バックトラックによる正規表現マッチングの計算量判定の実装2018

    • 著者名/発表者名
      高橋 和也, 南出 靖彦
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ
  • [学会発表] 先読み付き正規表現と解析表現の微分2018

    • 著者名/発表者名
      Takayuki Miyazaki, Yasuhiko Minamide
    • 学会等名
      第21回プログラミングおよびプログラミング言語ワークショップ

URL: 

公開日: 2019-12-27  

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

Powered by NII kakenhi