9/10の予定

9/10の予定, 9/11の予定, 9/12の予定, 9/13の予定


10:30-17:30 PPLサマースクール 高階モデル検査とその応用 (241号室)

小林 直樹 東京大学 教授

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

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

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

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

13:00-17:00 WISS TOKYO (213号室)

ソフトウェア科学会 インタラクティブシステムとソフトウェアに関するワークショップ(WISS)は2012年12月に20周年を迎え、本研究分野においてこれまでに数多くの先進的な研究を社会に示してきました。これらの成果は実用化され広く普及しているものもあり、また2012年にはイグノーベル賞受賞者を輩出するまでに至っています。

WISSは年に一回開催されるワークショップですが、これまでに大都市圏を避けて開催してきたことと、参加者人数に限りがあるため、社会にその存在を十分にアピールできていませんでした。これに関しては、ワークショップの動画中継を他の学会・シンポジウムに先駆けて実施するなどの努力をしてきましたが、より多くの人々にWISSのことを知って頂くために、今回第30回記念大会となるWISSの上位組織であるソフトウェア科学会の大会の研究会企画として広く社会に開かれたイベントを開催いたします。

広告