Formal Models

Summer Semester 2016

Armin Biere, Andreas Fröhlich, Martina Seidl

News

Lecture on Thursday, June 9, 08:30 - 10:00, in HS 4.

Lecture on Thursday, April 21, 08:30 - 10:00, in HS 4.

Slides

Here you can find the 2016.1 of the slides and the slides on QBF (Q-resolution is not part of the exam) and the slides on SAT-based bounded model checking .

The slides will not be complete until the end of the lecture. Note: there is new content (BMC) which is also relevant for the exam.

The old German version is slightly out-dated but also still available as Foliensatz.

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.

Lecture Videos (from Summer Semester 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.