Formal Models

Summer Semester 2013

Armin Biere, Andreas Fröhlich, Martina Seidl


First lecture: Thursday, March 7, 08:30 - 10:00, HS 19.

Second lecture: Thursday, March 14, 08:30 - 10:00, HS 19.

Third lecture: Thursday, March 21, 08:30 - 10:00, HS 5 (different building).

Remaining lectures: Thursdays, 08:30 - 10:00, HS 19.


Here you can find version 2013.2 of the slides in English. Additional slides on QBF version 2013.2. Note that the slides on QBF are relevant for the exam!!! The slides will not be complete until the end of the lecture.

The old German version is slightly out-dated but also still available as Foliensatz.

There is no script nor book available at this point.


The lecture takes place on Thursday morning from 8:30 to 10:00. Exercises are on the same day in the afternoon.


Exercises will start on March, 7th with a preliminary meeting.

Exercises take place on Thursdays. Please consult the KUSSS page of this course for times, rooms and group assignments. Details on the organization can be found below.

  • Exercises of SS13 are not available on the web anymore.


Elevator simulation elsim.

Example implementations for EA in C: [ ]

Fast pattern matcher: posting, code.

Model Checking. E. Clarke, O. Grumberg, D. Peled. MIT press, 2000.

Modal and Temporal Properties of Processes. C. Stirling. Springer, 2001.

FSMCalc: Finite State Machine Calculator, Leopold Haller, JKU, 2006.