Winter Semester 2011
Inspection of exam (27.1.2012) is possible starting with the beginning of March (please contact Martina Seidl)
Next lecture and exercises: Thursday, 10th November
First exam: Friday, 27th January 2012, 10:15 - 11:45, HS 1
Thursday, 8:30 - 10:00, HS 9.
This lecture is a mandatory course in the Computer Science Master.
Teaching language is English.
This is version 2011.4.
[ 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 will also start in the first week on October 6.
Times, rooms and group assignments may be found on the KUSSS page of this course. Details on the organization of the exercises may be found below.
A. Biere. Tutorial on Model
Checking, Modelling and Verification in Computer Science.
V. D'Silva, D. Kröning, Daniel and G. Weissenbacher.
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.
C32SAT is a satisfiability checker for boolean C expressions. It can check whether they can be satisfied, are tautological, or can potentially be undefined according to the C99 standard.