|
プログラム理論特論_E
|
|
| Instructor(s) |
Tetsuya Mizutnai, Yukiyoshi Kameyama
|
| Mizutani: mizutani (AT) cs.tsukuba.ac.jp, Kameyama: kam (AT) cs.tsukuba.ac.jp | |
| URL | |
| Office hours | Office hours will be announced at the first lecture. |
| Cource# | 01CH213 |
| Area | Intelligent Software |
| Basic/Advanced | |
| Course style | Lecture |
| Term | Fall A |
| Period | Fri5,6 |
| Room# | |
| Keywords | Symbolic Logic, Specification, Verification, Semantics, Hoare Logic, Realtime System. |
| Prerequisites | Familiarity with propositional/predicate calculi (logic) and fundamentals of programming languages will be helpful, though not necessary. |
| Goal | |
| Outline | Logic plays an important role in the study of software science. In this course, we study logic for specification and verification of programs. |
| Course plan | 1. Foundation of the first-order predicate calculus (Mizutani). 2. Formal specification of programs by Hoare Logic (Mizutani). 3. Formal verification of programs by Hoare Logic (Mizutani). 4. Formal specification of realtime systems (Mizutani). 5. Formal verification of realtime systems (Mizutani), Applications to Program verification (Kameyama). |
| Textbook | |
| References | M. Huth and M. Ryan, "Logic in Computer Science (Second Edition)", Cambridge Univ. Press, 2004. |
| Evaluation | On the basis of (1) attendance to the lectures, and (2) the scores of reports and in-class exercises. No examination. |
| TF / TA | |
| Misc. | |