[  news | slides | schedule | exercises | recordings | resources ]

Formal Models

Summer Semester 2020

Armin Biere, Daniela Kaufmann

News

• Exercises start on March 19
• Infos on Course Organization

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

Slides

Here you can find version 2020.3 of the slides.

Schedule

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

Exercises

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

• Exercise 1
• Exercise 2
• Exercise 3
• Exercise 4
• Exercise 5
• Exercise 6
• Exercise 7
• Exercise 8
• Exercise 9
• Exercise 10

Lecture Videos (from Summer Semester 2014)

• Lecture 06. March 2014
• Lecture 13. March 2014
• Lecture 20. March 2014
• Lecture 27. March 2014
• Lecture 03. April 2014
• Lecture 10. April 2014
• Lecture 08. May 2014
• Lecture 15. May 2014
• Lecture 22. May 2014
• Lecture 05. June 2014 (supplementary)
• Lecture 12. June 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.

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.