1/24（木）

14:00-14:15        オープニング（開催挨拶・自己紹介）

14:15-15:15        セッション1：自動修正（司会：早水公二）

• 関数型プログラムのための反例による条件式の自動修正：松井健（九州大学）
• NuSMV の反例生成に基づいたステートマシン図の自動修正：栗田聖也，井川直，横川智教，有本和民（岡山県立大学）

15:15-15:30        休憩

15:30-16:00        セッション2：導入・教育(1)（司会：早水公二）

• NuSMV のモデル生成を支援するプログラミング環境についての一検討：内藤駿人，井川直，横川智教，有本和民（岡山県立大学）

16:00-16:30        休憩

16:30-17:30        セッション3：導入・教育(2) （司会：早水公二）

• 工業高専生への導入を目的としたB-Methodのモデル記述（２）：大西孝臣（苫小牧高等専門学校）
• 宇宙用途のFPGA外部インターフェース回路開発に対するモデル検査適用：倉林翔，梅田浩貴，石垣雄基，植田泰士（宇宙航空研究開発機構）

1/25（金）

10:00-10:30       セッション4：モデル検査の応用利用（司会：横川智教）

• 記号モデル検査を用いたインフラストラクチャーにおける障害伝搬の解析について：土屋達弘（大阪大学）

10:30-11:15        全体ディスカッション（司会：横川智教）

11:15-11:25        クロージング