Coqで学ぶ定理証明入門(7/12開催)[終了]

■日 程:2011年7月12日(火)
■会 場:国立情報学研究所 20階ミーティングルーム(2009, 2010)
■講 師:(有)ITプランニング 今井宜洋

セミナー概要
日 時 2011年7月12日(火) 10:00-17:00(9:30受付開始)
会 場 国立情報学研究所 20階 ミーティングルーム1・2(2009, 2010)
概 要 ソフトウェアの不具合を防ぐ技術として定理証明器を使った検証技術が着目されています。定理証明器は実際に動作するプログラムのふるまいを保証できる形式手法です。特にその一つであるCoqは強力な仕様記述能力を持ちながら、証明を支援する機構を備えています。本セミナーでは、検証技術の基本からCoqを使った関数型プログラミングのテクニックと、タクティックを使った証明の技法までを学びます。さらに、企業での取り組みや例題を交えながら既存のプロジェクトで運用するときの問題や注意点について考えていきます。

なお、本セミナーでは、会場に設置されたシンクライアントを使いCoqの演習を行います。もし、ご自身のPCで演習されたい場合は、下記を参考にCoqの環境をインストールし、ご持参ください。
http://www39.atwiki.jp/fm-forum/pages/16.html

内容のレベル 入門、形式仕様記述
講 師 (有)ITプランニング 今井宜洋
対 象 一般 ※ 定員 36 名(先着順)
参加費 一般会員 無料、一般非会員 16,000円(税込み)
学生会員 無料、学生非会員 8,000円(税込み)
※会費の一割は、東日本大震災の義援金に寄付いたします。
※NPO法人 トップエスイー教育センター、日本ソフトウェア科学会の会員の方は割引の対象となります。
受講料は当日受付にて現金でお支払いください.その他の支払い方法をご希望の方は,事前にメールで inquiry@topse.or.jp までお知らせください.
主 催 NPO法人 トップエスイー教育センター
協 力 国立情報学研究所 GRACEセンター
協 賛 日本ソフトウェア科学会 ソフトウェア工学の基礎研究会
お問合せ先 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp