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, Guarded commands, Non-determinacy
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. Introduction to Hoare Logic, formal specification and verification of programs (Mizutani).

2. Formal verification of programs by Hoare Logic (Mizutani).

3. Hoare Logic as a formal theory system (Mizutani).

4. Formal semantics of programs, treatment of arrays in Hoare Logic (Mizutani).

5. Formal specification and verification of nondeterministic systems with guarded commands (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