| 日時(Date) | 平成30年6月5日（火）4限（15:10--16:40) Tue. June 5th, 2018, 4th Period (15:10--16:40) |
|
|---|---|---|
| 場所(Location) | L1 | |
| 司会(Chair) | Raula Gaikovina Kula 助教 (Assist. Prof. Raula Gaikovina Kula) | |
| 講演者(Presenter) | アフェルト レナルド (産業技術総合研究所 情報技術研究部門 主任研究員) | |
| 題目(Title) | 定理証明支援系Coqによるソフトウェア・数学の形式検証 | |
| 概要(Abstract) | ソフトウェアや数学の証明に誤りのないことを保証するのは重要な研究課題で ある．1970年代からカリー＝ハワード同型対応に基づく形式体系の研究が継続 的に行われてきた．その形式体系が定理証明支援系という形式検証ツールとし て実現された結果，厳密で現実的な形式検証が可能となった．例えば，クリティ カルな基盤ソフトウェア（コンパイラやオペレーティングシステム等）と大規 模な数学の証明（四色定理やケプラー予想等）の形式検証が近年相次いで成功 し，IT業界でも形式検証はスマートカードの厳密な安全性評価に応用されてい る．本発表では，ソフトウェアと数学の形式検証の実例を通じて，定理証明支 援系による形式検証の基本を説明する．特に，ACMによる受賞を契機に注目を 集めているフランス国立情報学自動制御研究所（INRIA）で開発されているCoq という定理証明支援系を紹介する． | |
| 講演言語(Language) | 日本語(メイン)・英語 | |
| 講演者紹介(Introduction of Lecturer) | 2004年東京大学大学院情報理工科学研究科・コンピュータ科学専攻博士課程修 了．現在，産業技術総合研究所・情報技術研究部門・サイバーフィジカルウェ ア研究グループ主任研究員．定理証明支援系Coqを用いて，安全なソフトウェ アの構築方法を研究している．暗号スキームやセキュリティプロトコルや情報・ 符号理論への応用を目標として，アセンブリやC言語などの低レベルのプログ ラムの形式検証とセキュリティ用の数学の形式化を研究している． | |
| 講演資料(Slide) | 180605.pdf |