Seminar: Theoretical Foundations of Model Checking - winter term 06/07

overview

description

Owing to the increasing complexity of embedded systems - first-class cars for example contain several dozens of CPUs interacting with each other - the need
for formal verification methods is growing. Many such systems
are used for safety criticial applications which adds to this need.

Model Checking is a method for proving properties of a system, specified using
mathemtical logics.

Since the beginning of model checking in the 80s there is considerable progress
in this field. Today, all important hardware manufactures have adopted
model checking techniques.

comment

In this course, we will focus on the theoretical foundations of model checking.

Topics include the characterization of bisimilarity, as well as hybrid automata.

Participiants should have some knowledge about mathematical logics and theoretical computer science.