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

Printed handout (introductory material + slides).
1up handout.

Slides

Exercises and past exam questions

Exercises and solutions.
Relevant old exam questions (eventually needs to be updated with 2015 questions).

Sources

TLMC.tar.gz (README).