皆様、
＃複数受け取られましたらご容赦ください．
東北大学の小林と申します．
当研究室では現在，高階モデル検査（高階再帰スキームのモデル検査）と そのプログラム検証などへの応用をテーマとした研究を精力的に進めており， プロジェクトに携わるポストドクの研究員を探しております．
身近にご興味のある方がいらっしゃいましたら，8月15日（必着）までに小林 (koba@ecei.tohoku.ac.jp) までメールでお知らせいただければ幸いです。 その際、できれば略歴および論文リスト（フォーマット自由）もメールに添えるか または郵送でお送りください。 （後日、さらに詳細な資料をお願いする可能性があります）．
募集の条件は概ね以下のとおりです。
================ 着任時期：2011年10月〜2012年4月の間（さらに数ヵ月の前後は応相談）
任期：年度単位の更新で、業績により最長2016年3月まで延長可能
給与：月額30〜35万円程度（大学の規定による．細かい条件は応相談）
研究テーマ： 高階モデル検査（高階再帰スキームのモデル検査）および、 そのプログラム検証やデータ圧縮への応用。
高階モデル検査については，下記のプロジェクトの概要および， 小林らによる最近のPOPL 2009/2010やPLDI 2011, LICS 2009等の論文を ご覧ください。
条件： - 着任時に博士号を取得していること
- 理論計算機科学全般に明るいこと．
- 以下の中の２つ以上のトピックに詳しいか、または １つ以上のトピックに詳しくプログラミング能力が特に高いこと
モデル検査（特にソフトウェアモデル検査） 型システム ゲーム意味論 プログラム解析 オートマトンと形式言語理論 自動定理証明 (可逆)データ圧縮技術
問い合わせ先： 小林直樹 東北大学大学院情報科学研究科情報基礎科学専攻 〒980-8579 仙台市青葉区荒巻字青葉6-3-09 TEL: 022-795-7177 FAX: 022-795-7526 Email: koba@ecei.tohoku.ac.jp
====================== 研究プロジェクトの概要 ======================
モデル検査はシステムが与えられた性質を満たすか否か網羅的に検証する手法 であり，近年ハードウェアやソフトウェア検証の分野で大きな成功を修めてい る．高階モデル検査は，検証対象のシステムとして無限木を記述する高階文法 を扱うものであり，従来の有限状態モデル検査やプッシュダウンモデル検査の 真の拡張になっている．
最近になって，我々は，高階モデル検査が高レベルプログラムの自動検証に有 用であることを示すとともに，高階モデル検査問題が多重指数関数完全の計算 量クラスに属するにもかかわらず，多くの入力に対して現実的な時間で動作す るようなモデル検査アルゴリズムを考案し，世界初の高階モデル検査器の実現 に成功した．さらに，それに基づいて関数型言語MLの小さなサブセットに対す るソフトウェアモデル検査器を実現した．
本研究プロジェクトでは，上記の成果をさらに発展させ，
（１）高階モデル検査の理論および実装技術の発展による，より高速な高階 モデル検査器の実現
（２）関数型言語やオブジェクト指向言語に対するソフトウェアモデル検査器 （つまり高階モデル検査に基づくプログラム自動検証器）の実現
（３）データ圧縮など，高階モデル検査の新たな応用分野の開拓
を目指す．