TUD Logo

TUD Home » ... » Teaching » Winter Term 2015/16 » Lecture “Model Checking”

Chair of Algebraic and Logical Foundations of Computer Science

Lecture “Model Checking” (4/4/0)

Prof. Dr. Baier and Dr. Klüppelholz

Language: English

Description

Model Checking is a fully automatic verification method for reactive systems. This course provides an introduction to the main principles of model checking:

  • modeling reactive systems by transition systems
  • linear time properties and Büchi automata
  • linear temporal logic and automata-based model checking
  • computation tree logic

and selected topics of:

  • bisimulation and simulation relations
  • probabilistic and timed automata
  • partial order reduction, symbolic model checking

Dates

Thu 2. and 3. time slot [09:20 am – 12:40 pm] APB/E05
Fri 2. and 3. time slot [09:20 am – 12:40 pm] APB/E05

The first lecture will be held on Thursday, October 15th at 09:20 am. The date of the first tutorial will be announced in the lecture. There will be no fixed assignment of the lectures and exercises to time slots. The schedule for the lectures and tutorials will be announced every week.

The course consists of a (4/2/0) lecture with exercises for the theoretical foundations (October – December) and an introduction to model checkers with practical exercises (0/2/0) (January).

Prerequisites

For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.

Creditability

Bachelor Informatik
INF-B510: Vertiefung
INF-B520: Vertiefung zur Bachelorarbeit
Master Informatik
INF-BAS6: Basismodul Theoretische Informatik
INF-VERT6: Vertiefungsmodul Theoretische Informatik
Diplom Informatik
INF-BAS6: Basismodul Theoretische Informatik
INF-VERT6: Vertiefungsmodul Theoretische Informatik
Master Computational Logic
MCL-TCSL: Theoretical Computer Science and Logic

Mailing list

Students are advised to subscribe to the mailing list of the lecture.

Contact

In case of questions or problems please contact Dr. Klüppelholz.

Last modified: 30th Nov 2016, 2.54 PM
Author: Dipl.-Inf. Steffen Märcker