[Back to Teaching]

Mathematical Structures in Formal Methods (AY 2024)

General

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

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

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