■日 程：2012年3月22日(木) 10:30-18:00
3月23日(金) 10:30-16:15（2日間）
■会 場：国立情報学研究所 20階 ミーティングルーム1・2（2009・2010）
※定員に達したためお申込を締め切りました。
3月23日(金) 10:30-16:15（2日間）
■会 場：国立情報学研究所 20階 ミーティングルーム1・2（2009・2010）
※定員に達したためお申込を締め切りました。
セミナー概要
| 日 時 | 2012年3月22日(木) 10:30-18:00、 3月23日(金) 10:30-16:15（2日間） |
|---|---|
| 会 場 | 国立情報学研究所 20階 ミーティングルーム1・2(2009, 2010) 〒101-8430 東京都千代田区一ツ橋2-1-2 |
| 概 要 | ソフトウェアの不具合を防ぐ技術として，定理証明器を使った検証技術が注目されています．この技術は形式手法の一種であり，実際に動作するプログラ ムのふるまいが正しいことをを保証することができます．同じく形式手法に分類されるモデル検査技術と比較して，潜在的な適用範囲ははるかに広く強力な手法 ですが，その分使いこなすには熟練が必要であると言われています．本講義では，定理証明器の一つであるCoqをとりあげます．Coqは，強力な仕様記述能力を持ち，また証明を支援する機構を備えています．講義は検 証技術の基本から始め，Coq を使った関数型プログラミングの手法やタクティックを使った証明の技法を学んでいきます．さらに，企業での取り組みや例題を交えながら実際のプロジェクト に適用する際の問題点や注意点についても紹介します．その際，講師自身が開発した，Java や Scala と連携するためのcoq2scala 機能を使用して，証明されたプログラムを既存のプロジェクトに導入する方法についても説明します．
【前提知識】 【講義スケジュール】 【講 師】 ※フィードバックをいただく目的で，参加費を無料に設定させていただいております．講義終了後のアンケートにご協力ください． |
| 内容のレベル | 入門 |
| 参加費 | 無料 ※NPO法人 トップエスイー教育センター会員は優先的にご参加いただけます。 |
| 定 員 | 30名(先着順) ※定員に達し次第，申し込みを締め切らせていただきます。 |
| 申込方法 | 参加申込みサイトより必要事項を入力の上、お申込みください。 ※定員に達したためお申込みを締め切らせていただきました。 |
| 主 催 | 国立情報学研究所 GRACEセンター, NPO法人 トップエスイー教育センター |
| お問合せ窓口 | セミナーに関するご質問などは、下記アドレスにて承ります。 inquiry@topse.or.jp |