Formal Models

Summer Semester 2021

Armin Biere, Nils Froleyks, Daniela Kaufmann, Martina Seidl

News

Lecture and Exercises will be online through the whole semester.
Infos on Course Organization; The presentation of the course organisation will take place on March 11, 9:00, before the first Q & A session.

Slides

The recent slides will be published in Moodle during the semester. Here you can find version 2020.3 of the old slides.

Schedule

For the lecture videos will be provided (links in Moodle). There is a live Q& A session every Thurdsay from 9:15-10:00. The course organization will be explained on March 11, 9:00 in Zoom.

Exercises

Exercises take place virtually. Details can be found in the slides on the course organization.

Old Lecture Videos (from Summer Semester 2014)

Recent lecture recordings will be published in Moodle. As the content is overlapping, it also makes sense to watch part of the old videos.

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.

Resources

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: [ faimpl.zip ]

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.