Program verification is a fundamental theory in proving correctness of a program. Model checking is an important and popular technique for automatically verifying correctness properties of finite-state systems. This course mainly focuses on the fundamental principles and methods for model checking. This course includes the syntax and the semantics of linear temporal logic (LTL), the syntax and the semantics of computation tree logic (CTL), principles of reasoning-based program verification, and methods of model checking in applications etc.
- 教师: 张小旺