# Temporal Logic and Model Checking

**A course of 8 lectures prepared
by Mike Gordon for CST
Part II**

Last given in 2015
(webpage); now
discontinued.

**Summary:** State transition systems. Representation of state
spaces. Reachable states. Checking reachability
properties. Fixed-point calculations. Symbolic methods using binary
decision diagrams. Finding counter-examples. Various uses of
reachability calculations. Temporal properties. Linear and branching
time. Path quantifiers. Temporal logic. Brief history (Prior to
Pnueli). CTL and LTL. Model checking. Simple algorithms for verifying
that temporal properties hold. Reachability analysis as a special
case. Simple software and hardware examples. PSL and assertion based
verification. Comparison of verification by dynamic simulation and
static formal verification. Very brief introduction to recent
developments, e.g. Counter-example guided abstraction refinement
(CEGAR).

**Reading**

**Slides**
**Exercises and past exam questions**

**Sources**