Temporal Logic Model Checking

Overview

This course introduces the basic concepts of functional verification and model checking, highlighting their importance in modern system designs. It explains different modeling formalisms for representing the behavior of hardware and software, which are either suitable for automated analysis or can represent data-dependent controls that are common in computing system designs. Additionally, it describes system compositions with respect to different communication models. This course can also be taken for academic credit as ECEA ####, part of CU Boulder’s Master of Science in Electrical Engineering.

Syllabus

Linear Time Properties

This module introduces concepts of linear-time interpretation of transition systems, and shows how to specify various types of properties on the linear-time behavior.

Linear Time Logic

This module introduces linear-time logic (LTL) for specifying linear-time properties and framework for deciding truth of LTL formulas with respect to transition systems.

Computation Tree Logic

This module introduces computation tree logic (CTL) for specifying properties and model checking algorithms for deciding truth of CTL formulas with respect to transition systems.

Symbolic CTL Model Checking

This module introduces basic concepts of symbolic model checking, how transition systems can be encoded as switch functions, mode checking algorithms based on switch functions, and BDDs as a compact representation of switch functions.