[ new | Schedule | overview | slides | exercises | resources ]

Model Checking

Winter Semester 2010

Armin Biere, Florian Lonsing

News

Second exam, 1st April 2011, 08:30 - 10:00, T 211

First exam Thursday, 27th January 2011, 08:30 - 10:00, HS 9

added link to article on Bloom filters to resources

Schedule

Thursday, 8:30 - 10:15, HS 9.

Overview

This lecture is a mandatory course in the Computer Science Master.

Teaching language is English.

Slides

This is version 2010.7.

[ mcslides.pdf ]

We will upate the slides during the semester and they are not considered to be complete until the end of the semester.

Exercises

Exercises will also start in the first week on October 7.

Times, rooms and group assignments may be found on the KUSSS page of this course.

Grading in exercises is based on the quality of written homeworks and presentations in class. There is no final exam. Please see also information about course organization below.

• Course Organization
• Assignment 1
• Assignment 2
• Assignment 3
• Assignment 4
• Assignment 5
• Assignment 6
• Assignment 7
• Assignment 8
• Assignment 9
• Assignment 10 (UPDATE: 17.12.2010)
• Assignment 11
• Supplementary Exercises

Resources

A. Biere. Tutorial on Model Checking, Modelling and Verification in Computer Science.
In Proc. 3rd Intl. Conf. on Algebraic Biology (AB'08), Lecture Notes in Computer Science (LNCS), vol. 5147, Springer 2008.

V. D'Silva, D. Kröning, Daniel and G. Weissenbacher.
A Survey of Automated Techniques for Formal Software Verification.
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD), Vol. 27, No. 7, pages 1165-1178. July 2008.

Model Checking: Algorithmic Verification and Debugging. Communications of the ACM, November 2009.

SPIN Model Checker. The Primer and Reference Manual. G. Holzmann, Addison Wesley, 2004.

Space/time trade-offs in hash coding with allowable errors. B. Bloom, Communications of the ACM 13 (7), 1970.

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.

Evaluation code for various string hash functions: testhash.c.

ElSim: elevator simulation.

Boolean satisfiability. From theoretical hardness to practical success. Communications of the ACM, August 2009.

R. Brummayer, A. Biere. Local Two-Level And-Inverter Graph Minimization without Blowup. In Proc. 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'06), Mikulov, Czechia, October 2006.

AIG implementation and visualization: aig4teaching.zip, lg-0.9.tar.gz.

BDD implementation and visualization: bdd4teaching.zip, lg-0.9.tar.gz.