CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コース ・ニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

研修コース「 Agda による仕様記述」開催のお知らせ


コース概要

近年、体系的にシステムを開発する手段の一つとして数理的技法(形式手法)が注目を集めています。例えば形式仕様記述の枠組みを使うと、仕様や設計から曖昧さをなくし、全体の整合性を保証することができます。結果として設計書や実装に不具合の種が入り込むことを防ぐことができます。
本コースでは、形式仕様記述の概要とその実際を講義と演習を通して実感して頂きます。演習環境として用いるツール Agda は(1)関数型プログラミング言語(2)形式仕様の処理系(3)定理証明支援系の側面を持つツールです。本コースでは(1)(2)の側面を使い、抽象的なデータの定義と関数を用いてシステムを記述すること、記述を支援する Agda の機能と操作法を扱います。演習の時間を多くとり、実例と経験から形式仕様記述を理解できるコースとなっています。

目標

(1)厳密に定義されるデータと関数でシステムを記述することの利点・意義を理解する。
(2)Agda を使って簡単なプログラムを記述できるようになる。
(3)Agda を使い、データと関数を用いてシステムを整合的に記述できるようになる。

受講者対象・受講条件

本コースは Agda によるプログラミング、仕様記述に興味がある技術者、マネージャ、学生の方々を対象とします。
受講には以下の条件を課させて頂きます:

講師

産業技術総合研究所システム検証研究センターの研究員 

研修期間

三日間のコースを 10月、11月に一度ずつ開催します。

A. 10/13(火) 13:00〜17:00 ,  10/14(水)〜15(木) 10:00〜17:00 終了

B. 11/10(火) 13:00〜17:00 ,  11/11(水)〜12(木) 10:00〜17:00 終了

費用

試行開催のため無料。

定員

6名 → 10名 (定員になりましたので受付を締め切りました)

会場

産業技術総合研究所 関西センター (大阪府池田市)

コース内容

受講申し込み

お問合せ

 研修コース事務局
 問い合わせフォーム

産総研ホーム > 組織 > 研究センター > システム検証研究センター
Copyrights (C) 2005-2009 AIST Research Center for Verification and Semantics, All Rights Reserved.