発表概要
- 発表時間は質疑込みで 30 分です．
- 発表時間と質疑との配分は発表者がご自由に設定してください．
第1日目 1月18日(木)
14:00‐14:05 オープニング
14:05‐15:05 セッション1：モデル化
- シンボリック実行に基づく状態遷移表の抽出手法の提案
山本椋太，清水貴裕，吉田則裕（名古屋大学）
- ロールベースアクセス制御に向けたフォーマルなモデルの検討
綿貫凌，大森洋一，荒木啓二郎（九州大学）
15:05‐15:15 休憩
15:15‐16:15 セッション2：定理証明・その他
- 機械学習を用いた Coq 上の命題論理の自動証明
金原雅典，佐藤亮介，鵜林尚靖，亀井靖高（九州大学）
- 形式手法は何を目指しているのか，何を目指すべきなのか
山田隆弘（宇宙航空研究開発機構宇宙科学研究所）
16:15‐16:30 休憩
16:30‐17:30 セッション3：SAT・SMT の応用
- MathSAT を用いた safe Time Petri Net の非有界モデル検査手法
井川直，横川智教，佐藤洋一郎，有本和民（岡山県立大学），近藤真史，宮崎仁（川崎医療福祉大学）
- ハックの自動発見について
土屋達弘（大阪大学）
第2日目 1月19日(金)
09:30‐11:00 セッション4：教育
- 工業高専生への導入を目的とした B-Method のモデル記述(1)
大西孝臣（苫小牧高等専門学校）
- モデル検査向け教育用ビジュアルプログラミング言語の開発
山下誠治，角田雅照（近畿大学），横川智教（岡山県立大学）
- モデル検査コンテストについて
早水公二（フォーマルテック）
11:00‐11:30 全体ディスカッション及びクロージング