Key components of hardware and software can be modelled as finite-state transition systems. With a temporal logic one can formulate interesting runtime properties of such a system. The term model checking was coined in the early eighties for a software which implements a decision procedure for such formulae. However, such decision procedures suffer from the state explosion problem; each extra bit of state information doubles the state space and typically also the runtime. Worse still, decision procedures for the more expressive temporal logics are known to be PSPACE-hard.

Significant effort has been put into the optimization of decision procedures and the reduction of state spaces to make model checking applicable for real-life problems. Today's model checkers have increased the manageable state space size from several to several hundred bits and are in wide industrial use.

In this seminar we try to give an overview of this development. This seminar will be held in english; each student presents a topic in a 45-minute talk and a written report.