プログラム理論特論_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. 
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 inclass exercises. No examination. 
TF / TA  
Misc. 