本文へジャンプ

  • HOME
  • 講演会情報

講演会情報

高階モデル検査とその応用
講演者:小林直樹(東北大学情報科学研究科)
平成23年6月29日(水)16時30分〜18時 東京大学理学部七号館214講義室
モデル検査はシステムが与えられた性質を満たすか否か網羅的に検証する手法であり,近年ハードウェアやソフトウェア検証の分野で大きな成功を収めている.高階モデル検査は,検証対象のシステムとして無限木を記述する高階文法を扱うものであり,従来の有限状態モデル検査やプッシュダウンモデル検査の真の拡張になっている.

本講演では,高階モデル検査問題とその主要な結果について解説した後,プログラム検証やデータ圧縮に関する様々な問題が高階モデル検査問題に帰着できることを示す.つづいて,高階モデル検査問題がプログラミング言語における型推論の問題に帰着できることを示す.さらに,その帰着を用い,高階モデル検査問題がn重指数時間完全(nは高階文法のオーダー)であるにもかかわらず,多くの問題について現実的な時間で解くことができるアルゴリズムを与え,実際にそれに基づいて構築されたプログラム検証器のデモを行う.最後に高階モデル検査に関する研究の今後の展望を述べる.