Formal Methods
Course overview
This graduate-level course (40 hours, 2 credits) covers the fundamental theories and key techniques in formal methods research. Students will learn how to construct abstract models of software systems, specify their properties using temporal logic, and verify those properties through rigorous methods. The major topics include:
- Abstract models of programs and software systems: transition systems, operational semantics, and modelling concurrent systems.
- Deduction-based verification: Hoare logic, weakest preconditions, and proving program correctness via deductive reasoning.
- Temporal logic: linear temporal logic (LTL), computation tree logic (CTL), and their expressiveness for specifying system properties.
- Model checking: algorithmic verification of finite-state systems against temporal logic specifications.
By the end of the course, students are expected to understand the core ideas of formal methods, be familiar with major results in software system analysis and verification, and develop research skills in this area.
Prerequisites
- Mathematical Logic and Program Theory
- Formal Languages and Automata Theory
Syllabus
| Topic | Hours | Instructor |
|---|---|---|
| Introduction | 3 | Xueyang Zhu |
| Programs and Software System Models (1) | 3 | Xiaomu Shi |
| Deduction-based Verification | 9 | Xiaomu Shi |
| Programs and Software System Models (2) | 12 | Xueyang Zhu |
| Temporal Logic | 9 | Xueyang Zhu |
| Model Checking | 2 | Xueyang Zhu |
| Course Summary | 1 | Xueyang Zhu |
References
- The Foundation of Program Verification, J. Loeckx and K. Sieber, Wiley & Sons, 1984
- Model Checking, E. M. Clarke, O. Grumberg and D. Peled, MIT Press, 1999
- Software Reliability Methods, D. A. Peled, Springer-Verlag, 2001
- Principles of Model Checking, C. Baier and J.-P. Katoen, MIT Press, 2008
- Verification of Sequential and Concurrent Programs, K. R. Apt, F. S. de Boer and E.-R. Olderog, Springer-Verlag, 2009