Formal Models

Summer Semester 2012

Armin Biere, Andreas Fröhlich, Martina Seidl


No lecture and exercises on June 14

On June 21, there are exercises.

On June 28, the lecture will take place (not relevant for the exam on the same day, but for the exams in autumn).

Appointments for the tests of the exercise classes:

  • Thursday 3.5. 2012: 20:00
  • Thursday 21.6. 2012: 17:15 or 9:00
  • Wednesday 27.6. 2012: 17:15

Room change for exercise class at 12:00. New location T112

First lecture: March 8, 08:30 - 10:00, HS 9.


Here you can find version 2012.1 of the slides in English. The slides will not be complete until the end of the lecture.

The old German version is 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 in HS 9. Exercises are on the same day in the afternoon.


Exercises will start on March, 8th 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.


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.