トップエスイー特別講義：CafeOBJで学ぶ形式仕様記述とその証明(10/23,30)

(1日目) 2015年10月23日(金) 13:30-17:00(受付開始:13:00)
(2日目) 2015年10月30日(金) 13:30-17:00

国立情報学研究所 国立情報学研究所 20階 ミーティングルーム(2009/2010)

　CafeOBJは、代数的にシステムの仕様を記述し、その上の性質を証明することができる先端的な形式仕様言語の一つです。本講義では、CafeOBJを使った代数仕様言語の記述方法とシステムの性質を対話的に証明する方法を実際に支援ツールを使いながら学ぶことができます。
　講義は2日間にわたって行われ、自然数やリストを使ったCafeOBJによる代数仕様記述の記述方法から、具体的な相互排他プロトコルを使った対話的な証明まで、ツールを通して体験していただけます。CafeOBJの開発者の一人である二木特任教授から直接学ぶことができるまたとない機会となっております。
　当日会場に用意されたシンクライアントにて演習を行うことができます。ご自身のPCで動かしてみたいという方は、以下のページからCafeOBJ 1.5.3をインストールしてご持参ください。http://cafeobj.org/download/

10月23日(金)
13:30 – 15:00 講義1: CafeOBJの概要と基礎, 自然数の表現
15:15 – 16:45 講義2: モジュール構造とジェネリックリスト
16:45 – 17:00 質疑応答

10月30日(金)
13:30 – 15:00 講義3: CafeOBJによるモデリングと記述の実際
15:15 – 16:45 講義4: CafeOBJによる証明の記述と証明の実際
16:45 – 17:00 質疑応答

以下のページから最新の講義資料をダウンロードできます。

http://www.jaist.ac.jp/~kokichi/lecture/1510NII/

※講義資料は英語が中心となりますが、講義は日本語で行います。

「CafeOBJ入門」
(1) 形式手法とCafeOBJ: http://ci.nii.ac.jp/naid/110006664762
(2) 構文と意味: http://ci.nii.ac.jp/naid/110006664763
(3) 等式推論と項書換システム: http://ci.nii.ac.jp/naid/110006840405
(4) 証明譜による検証法: http://ci.nii.ac.jp/naid/110006990888
(5) 認証プロトコルの検証: http://ci.nii.ac.jp/naid/130004549136
(6) 通信プロトコルの検証: http://ci.nii.ac.jp/naid/10025982447

北陸先端科学技術大学院大学 ソフトウェア検証研究センター 特任教授 二木厚吉

16名(先着順)
※定員に達し次第，申し込みを締め切らせていただきます。

NPO法人トップエスイー教育センター会員, トップエスイー受講生：無料
非会員：（一般）16,000円　（学生）8,000円
2日間通じての料金です。（1日のみ参加の場合も変わりません）

参加申込みサイトより必要事項を入力の上、お申込みください。
https://ws.formzu.net/fgen/S48854348/

NPO法人 トップエスイー教育センター

国立情報学研究所 GRACEセンター

セミナーに関するご質問などは、下記アドレスにて承ります。
inquiry_[at]_topse.or.jp ※_[at]_部分を@に変えてください