COEセミナーのお知らせ
平成17年4月18日
関係各位
２１世紀COEプログラム
－検証進化可能電子社会－
拠点リーダー 片 山 卓 也
ＣＯＥセミナーの開催について
4月27日(水）、下記のとおりＣＯＥセミナーを開催致します。
つきましては、多数の皆様にご参加いただきたく、ここにセミナーの案内を
申し上げます。
本セミナーに関しましては参加申し込み・予約等は必要ございませんので
直接、会場にお越しくださいますようよろしくお願い致します。
記
1. 日時 平成１７年４月２７日（水） １５：００～：１６：３０
2. 場所 情報科学研究科研究棟 Ⅲ棟５Ｆコラボレーションルーム６
3.講演題目 産総研システム検証研究センター紹介
4.講演者 （独）産業技術総合研究所 システム検証研究センター長
木下 佳樹 氏
5.講演要旨
発足後一年を迎えた産総研システム検証研究センター(Research Center for
Verification and Semantics, CVS)の運営方針と研究内容について紹介す
る。
CVSでは、プロジェクト毎に班を構成してネットワーク型の運営を行なっ
ているが、ヒエラルキー構造の研究チームも個人評価などのために用いている。
また、研究テーマを科学研究とフィールドワークに分けて考え、科学研究は学
術の価値観で、フィールドワークは技術が応用される社会での価値観で仕事を
行なうことにしている。
算譜意味論研究チーム（竹内泉チーム長）、自動検証研究チーム（高橋孝一副
センター長がチーム長を併任）、対話型検証研究チームの三つの研究チームを
構成している。科学研究テーマを研究チームに関連させて列挙すると以下のよ
うになる。
算譜意味論研究チームでは抽象化・詳細化を圏論的手法で研究するほか、リア
クティブシステムの代数構造と論理の研究、Kleene代数の研究などをすすめて
いる。自動検証研究チームではポインタ型を扱うプログラムの自動抽象化ツー
ル、および等式付木構造オートマトンによる自動検証器ACTAS などを研究開発
している。対話型検証研究チームではMartin-Lof型理論に基づく証明支援系
Agdaの研究開発をChalmers工科大学と共同で進めており、関連して
unificationによる項の推論を行なうmendori システム、Agda言語の簡約をお
こなうagateシステムなどを試作している。
以上の科学研究とは別に、フィールドワークプロジェクトをいくつか進めてお
り、そこからうまれた独自の検証手法を系統化する努力も開始したところであ
る。企業との共同研究では、あまり具体的なデータを公表できないので、CVS
で独自にソフトウェア開発プロジェクトを起こし、そのプロジェクトに、我々
が考案した手法を適用する実験も開始した。
6. 講演者略歴
1956年生。東京大学大学院理学系研究科博士課程情報科学専攻修了、理学博士
（情報科学専攻）。テキサスインスツルメンツ、電子技術総合研究所などを経
て、現在、独立行政法人産業技術総合研究所システム検証研究センター長。千
葉大学、筑波大学、東京大学などで非常勤講師として圏論の初歩を講義。
1992-3エディンバラ大学基礎計算機科学研究所客員研究員。算譜意味論、とく
に詳細化、抽象化の数理モデルの研究に携わる。
問合せ先 安心電子社会研究センター 桜井（内線：1261・E-mail:miyuki-s)
