[Back to Teaching]
Mathematical Structures in Formal Methods (AY 2024)
General
- Monday 10.45 - 12.15
- Face-to-face lectures at National Institute of Informatics (access). Room:
1212 1310A (call 03-4212-2652 in case of trouble reaching there)
- Lectures are in English
- Evaluation: Term-end report
- Registration from outside the Informatics Program, SOKENDAI: please first contact i.hasuo [at] acm.org (we need to arrange room access etc.)
Overview
Formal methods refer to a body of mathematical techniques used for guaranteeing correctness of computer systems. This course introduces the mathematical foundation of formal methods. Our technical focus will be on the theory of fixed points and a categorical theory of predicate transformers. These theories constitute the foundation of an abstract theory of model checking formulated in terms of coalgebras and fibrations, which we introduce in detail, too.
Objectives
- In-depth understanding of mathematical foundations of formal methods, especially the theory of fixed-point specifications
- Understand the mathematical theories used in the formalization of an abstract theory of formal methods, namely lattice theory and category theory
- Bridge the above mathematical foundations and actual implementations of effective formal verification algorithms (especially model checking algorithms)
Course structure
(1-3) Lattice theory, fixed point theorems
(4-6) Fibrations
(7-9) Coalgebras
(10-12) Categorical predicate transformers
(13-15) Model checking, formulated in categorical terms
References
- (A textbook will be distributed in the lectures)
Prerequisites
Familiarity with the following topics is desired (but not mandatory): formal logic, lattice theory, basic category theory
Schedule
Up-to-date schedule, handouts, and other information are available at the Attendant Portal Page (URL is shared with the registered attendants).