PPL サマースクール 2013(高階モデル検査とその応用)

講師:小林 直樹(東京大学)大学院情報理工学系研究科教授

講師:小林直樹(東京大学)

テーマ
高階モデル検査とその応用
日時
9月10日 10:30~17:30
講師
小林直樹(東京大学)
参加費
無料(参加者数把握のため事前登録をお願いする予定です)

モデル検査は、ハードウェアやソフトウェアの自動検証のための有望な技術として注目を集め、近年産業界にも応用が進んでいる。本チュートリアルでは、通常のモデル検査の拡張としてここ数年研究レベルで注目を集めている「高階モデル検査」とその応用について解説する。

通常のモデル検査では、検証対象のシステムを有限状態遷移システムとしてモデル化するのに対し、高階モデル検査では、検証対象のシステムを無限状態を持つ一種の高階関数型プログラムとしてモデル化する。これにより、従来のモデル検査よりもはるかに広い範囲のシステムを直接かつ自然にモデル化し、検証することができる。この利点を生かし、MLなどの高レベルプログラミング言語で記述されたプログラムの全自動検証器の開発が進んでいる。また、文字列や木構造データを、それを生成するプログラムとして圧縮すれば、高階モデル検査を利用することによって圧縮データを解凍することなくパターンマッチや変換を行うことができることもわかっている。形式言語理論の立場から見ると、高階モデル検査で扱うモデルは、文脈自由文法やインデックス文法を高階に拡張した文法であり、言語の階層構造、反復補題、等価性判定問題など多くの未解決の問題が残されている、理論的にも興味深い研究対象である。

本サマースクールでは、情報系の学部を卒業した大学院生および(大学・企業の)研究者を主な対象とし、高階モデル検査の基礎と、そのプログラム検証やデータ圧縮などへの応用について、未解決の研究課題にも触れながら解説する予定である。

なお、受講にあたっては、形式言語とオートマトン、プログラミング言語の基礎理論(特にλ計算と型システム)など、学部レベルのコンピュータサイエンスの知識を習得していることが推奨される。

幹事
千葉 滋(東京大学)
サーベイ
こちらのページ
広告