University of Tsukuba | Grad. Scho. Syst. and Info. Eng. | Dept. Comp. Sci. | List of Courses
Tetsuya Mizutnai, Yukiyoshi Kameyama
E-Mail Mizutani: mizutani (AT), Kameyama: kam (AT)
Office hours Office hours will be announced at the first lecture.
Cource# 01CH213
Area Intelligent Software
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.
relation degree program competence Knowledge Utilization Skills,Expert Knowledge
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. Preliminaries: Introduction to the first order logic, formal syntax and semantics of logic, mathematics and programs.

2. Formal syntax and semantics of while programs, partial correctness of while programs by Hoare Logic.

3. Total correctness of while programs and soundness of Hoare Logic.

4. Completeness of Hoare Logic, Proof outline.

5. Formal specification and verification of nondeterministic systems with guarded commands.


Apt, K. R., de Boer, F. S. and, Olderog, E-R. : Verification of Sequential and Concurrent Programs, 3rd edition, Springer-Verlag, 2009.
Class materials are distributed via manaba.


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 Based on the scores of reports and in-class exercises, assuming that students attend all lectures. No examination.
Misc. Japanese Course. There will be no TA not TF.