Formal Models

Summer Semester 2020

Armin Biere, Daniela Kaufmann


First lecture on Thursday, March 5, 08:30 - 10:00 in HS7.


Here you can find version 2020.3 of the slides.


The lecture took place on Thursday morning from 8:30 to 10:00 until we switched to an online only mode.


Exercises take place virtually through Moodle with two question and answer sessions each Thursday.

Lecture Videos (from Summer Semester 2014)

Note, that the video lecture from 05. June 2014 is considered additional material only this year and has no corresponding exercise.

Thus QBF and BMC will not be topics in the exam this year.


The slides on SAT/QBF BMC (old: slides on QBF and the slides on bounded models checking with SAT) are only considered supplementary material this year.

BMC Examples.

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.