注意: 本シラバスは，必要最低限の事項のみを記述した暫定版である．正式版は2012年3月中に発表する予定である．

1. 講座名

定理証明と検証

2. 　担当者

今井宜洋

3. 　単位数

1単位 (7コマ)

4. 実施時期

夏期集中

5. 講座概要

ソフトウェアの不具合を防ぐ技術として，定理証明器を使った検証技術が注目されている．実際に動作するプログラムのふるまいを保証できる形式手法である．同じく形式手法に分類されるモデル検査技術に比較して，潜在的な適用範囲ははるかに広く，強力な手法であるが，その分，使いこなしも難しい．特に本講義では，定理証明器の一つであるCoqをとりあげる．Coqは，強力な仕様記述能力を持ちつつ，証明を支援する機構を備えている．講義は検証技術の基本から始め，Coq を使った関数型プログラミングの手法やタクティックを使った証明の技法を学ぶ．さらに、企業での取り組みや例題を交えながら実際のプロ

ジェクトで運用するときの問題や注意点についても紹介する．