授業の目的 【日本語】
Goals of the Course(JPN) | | 高度で複雑な情報システムの動作の正しさを検証するため，数理論理学的モデルにもとづく検証支援ツールが実用化されている。本講義では，以下の2つのシステム検証手法を検証ツールの利用を通じて習得する。
(1)モデル検査：モデル検査ツールを用いて，システムの動作において指定される性質を満たさない動作例（反例）がないかどうかを検査することで効率的に不具合を発見する手法について学ぶ。
(2)定理証明：証明支援ツールCoqを用いて，計算機上での証明の記述・検証を体験する。この枠組のもとで，プログラムの正しさを数学的な厳密さで保証する手法について学ぶ。 |
|
|
授業の目的 【英語】
Goals of the Course | | Practical verification tools have been developed based on mathematical models to verify the correctness of complex information systems. This lecture explains the verification techniques of model-checking and theorem-proving for information systems using existing verification tools.
(1) Model Checking: Using model-checking tools, we learn how to efficiently find a faulty behavior from a program specification by searching counterexamples.
(2) Theorem Proving: Using the Coq theorem prover, we exercise how to describe proofs with computers. We learn how to show the correctness of a program. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN) | | | 高度で複雑な情報システムの動作の正しさを検証するため，数理論理学的モデルにもとづく検証支援ツールが実用化されている。本講義では，モデル検査と定理証明の2つのシステム検証手法を，実際に検証ツールを利用することを通じて習得し、利用によって情報システムの検証ができることを目的とする。 |
|
|
到達目標 【英語】
Objectives of the Course | | | We exercise to verify the correctness of information systems and learn how to mechanize the verification in practice, although it is generally an undecidable problem. This lecture gives the foundations for two well-known methods: model-checking and theorem proving, and provides the basic ideas for practical verification of information systems. |
|
|
授業の内容や構成
Course Content / Plan | | モデル検査と定理証明について解説し，それぞれ以下のとおり実際の検証ツールを用いた演習を行なう。
モデル検査：モデル検査ツールを用いて，システムの動作において指定される性質を満たさない動作例（反例）がないかどうかを検査することで効率的に不具合を発見する手法について学ぶ。
定理証明：証明支援ツールCoqを用いて，計算機上での証明の記述・検証を体験する。この枠組のもとで，プログラムの正しさを数学的な厳密さで保証する手法について学ぶ。
1. 導入
2. モデル検査の概要
3. モデル検査ツールを用いた演習
4. 定理証明系による検証
5. 定理証明系を用いた演習
6. 総括 | Providing essential explanations of model-checking and theorem-proving, we exercise the verification tools of model-checking and theorem-proving.
(1) Model-checking: Using model-checking tools, we learn how to specify the behavioral properties by temporal logic. The technique to derive counterexamples against the properties mechanically using well-known tools.
(2) Therem-proving: Using the Coq theorem prover, we exercise to describe proofs for software verification and prove theorems by Coq. We learn how to rigorously verify the correctness of programs with a mathematical method.
1. Introduction
2. Overview of Model-checking
3. Exercises of a Model-checking tool
4. Verification by theorem proving
5. Exercises of Coq Theorem-prover
6. Summary |
|
|
履修条件・関連する科目
Course Prerequisites and Related Courses | | | 論理学2c, オートマトン・形式言語および演習 | | Logic 2c, Automata and Formal Languages |
|
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | 演習課題の評価60％，レポート40％，合計100点満点で60点以上を合格とする。
情報システムをツールを用いて記述して数理モデルに基づく検証できることを評価の基準とする。 | 60% by the exercises given at each lecture and 40% by the term-end report assignment.
A student needs to be able to descript the requirements for information systems and test and verify the system efficiently using existing well-known model-checking tools and theorem provers. |
|
|
教科書・参考書
Textbook/Reference book | | | 必要に応じて資料を配布する。 | | The necessary materials are given in the lecture. |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | | 演習課題を出す。 | | We give exercises to improve understanding. |
|
|
授業開講形態等
Lecture format, etc. | | | 対面講義を基本とするが，状況に応じて遠隔配信を併用する場合がある． |
|
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|