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

Formal Models

Summer Semester 2017

Armin Biere, Daniela Ritirc, Martina Seidl

News

Exercises start on March 16
Details on the course organization of the exercises: Course Organization

First lecture on Thursday, March 9, 08:30 - 10:00, in HS 19.

Slides

Here you can find the 2017.1 of the slides and the slides on QBF and the slides on bounded models checking with SAT/QBF

The slides will not be complete until the end of the lecture.

Some exercises

There is no script nor book available at this point.

Schedule

The lecture takes place on Thursday morning from 8:30 to 10:00.

Exercises are on the same day in the afternoon.

Exercises

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.

• Course Organization
• 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
• Lecture 12. June 2014

Resources

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.