Mathematical Structures in Formal Methods (AY 2022)

General

Thursday 13.00 - 14.30
Remote lectures, live. Connection information has been sent by email.
Lectures are in English
Evaluation: Term-end report

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: 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).

Ichiro Hasuo