授業の目的 【日本語】
Goals of the Course(JPN) | | | 命令型プログラム・関数型プログラムを検証するための基礎理論および計算モデルについて理解することを目的とする。命令型プログラムについてはホーア論理による検証を紹介し，ループ不変条件の導出法や整数やリストに関する理論，論理式の充足可能性の判定手続きを紹介する。関数型プログラムについては計算モデルである項書換え系の停止性を証明する手法について講じる。 |
|
|
授業の目的 【英語】
Goals of the Course | | | We aim to learn a basis and computation models for verification of imperative or functional programs. For this purpose, a verification method based on Hoare logic is introduced for imperative programs, and then a method to compute loop invariants, theories for integers and arrays, and a method for satisfiability solving for some theories are introduced. For functional programs, a method for proving termination of a term rewriting systems, a computation model of functional programs is introduced. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN) | | | 論理式の意味論，制約式の充足可能性判定，プログラムを抽象化した計算モデル，プログラムを検証するための論理について学び，命令型プログラム・関数型プログラムを検証するための基礎理論および計算モデルに関する知識を修得する。 |
|
|
到達目標 【英語】
Objectives of the Course | | | We learn semantics of formulas, satisfiability solving for constraints, a computation model for programs, logics for program verification. Students are expected to understand a basis and computation models for verification of imperative or functional programs. |
|
|
授業の内容や構成
Course Content / Plan | | 充足可能性命令型プログラムについてはホーア論理による検証を紹介し，ループ不変条件の導出法や整数やリストに関する理論，論理式の充足可能性の判定手続きを紹介する。そのための基礎理論として命題論理，一階述語論理における意味論，充足可能性，帰納法について講じる。関数型プログラムについては計算モデルである項書換え系の停止性を証明する手法について講じる。
〔計画〕
1. 命題論理
2. 一階述語論理
3. 帰納法
4. 命令型プログラムの正当性検証
5. プレスブルガー算術式の真偽判定
6. ループ不変条件
7. 依存対法・依存対フレームワーク
8. まとめと評価
毎授業後に宿題を課し，次回時にレポートとして提出する。 | For imperative programs, a verification method based on Hoare logic is introduced, and then a method to compute loop invariants, theories for integers and arrays, and a method for satisfiability solving for some theories are introduced. As a basis of such subjects, propositional logic, first-order logic, satisfiability, and induction are introduced. For functional programs, a method for proving termination of a term rewriting systems, a computation model of functional programs is introduced.
1. Propositional Logic
2. First-Order Logic
3. Induction
4. Verification of Imperative Programs
5. A Decision Procedure for Presburger Arithmetics
6. Loop Invariants
7. Dependency Pair Method and Framework
8. Conclusion and Evaluation
At the end of every lecture, an assignment is proposed and the report is collected at the next lecture. |
|
|
履修条件・関連する科目
Course Prerequisites and Related Courses | | | 計算論基礎特論Aを受講していることが望ましいが、履修要件とはしない。 | | Basic Topic in Theory of Computation A is expected but not mandatory. |
|
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | | 講義後に与える演習課題の評価４０％，期末試験６０％，合計１００点満点で６０点以上を合格とする。理論や構造の基本的な概念を理解し，プログラム検証における計算モデルの位置付けを理解していることを合格の基準とする。 | | Examination 60% and assignment 40%. Credit is given if the total score is over 60%. A criterion to get the credit is to understand basic notions of theories and structures, and the contribution of computation models to program verification. |
|
|
教科書・参考書
Textbook/Reference book | | Aaron R. Bradley and Zohar Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
Enno Ohlebusch, Advanced Topics in Term Rewriting, Springer, 2002.
その他，必要に応じて指示，配布する。 | Aaron R. Bradley and Zohar Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
Enno Ohlebusch, Advanced Topics in Term Rewriting, Springer, 2002.
Other textbooks recommended to refer will be announced in a class and handouts will be delivered if necessary. |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | | 講義で学んだ理論を理解するための課題を与える。 | | Assignments to understand lectures will be presented at each class. |
|
|
授業開講形態等
Lecture format, etc. | | | 対面授業を実施する。状況に応じて，授業後にオンデマンドで視聴可能な講義ビデオを提供する。 |
|
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | | リアルタイムでの遠隔授業を実施するとともに，オンデマンドで視聴可能な講義ビデオを事前に提供する。 |
|
|