プログラム理論特論_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#  3B302 
Keywords  Symbolic Logic, Specification, Verification, Semantics, Hoare Logic, Guarded commands, Nondeterminacy 
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 
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. 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. 
Textbook 
Apt, K. R., de Boer, F. S. and, Olderog, ER. :
Verification of Sequential and Concurrent Programs, 3rd edition, SpringerVerlag, 2009. 
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  Based on the scores of reports and inclass exercises, assuming that students attend all lectures. No examination. 
TF / TA  
Misc.  Japanese Course. There will be no TA not TF. 