University of Tsukuba | Grad. Scho. Syst. and Info. Eng. | Dept. Comp. Sci. | List of Courses
プログラム理論特論_E
Instructor(s)
Tetsuya Mizutnai, Yukiyoshi Kameyama
E-Mail 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# 3B302
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 and verification of nondeterministic systems (Mizutani).

5. Formal specification and 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.

S. Hayashi, "Verification of Programs", Kyoritsu Shuppan Co., Ltd., 1995 (in Japanese).

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.
TOP