team |
[ new | Schedule | overview | slides | exercises | resources ] ## Model Checking## Winter Semester 2014## News## ScheduleLecture: Thursday, 8:30 - 10:00, S3 055 ## OverviewThis lecture is a course in the Computer Science Master. Teaching language is English. ## SlidesThis is version 2014.2. [ mcslides.pdf ] We will upate the slides during the semester and they are not considered to be complete until the end of the semester. ## ExercisesExercises start two weeks later. Organization will be announced at the end of the lecture on October 9th and/or can be found here. Times, rooms and group assignments may be found on the KUSSS
page of this course (342.236). - Course Organization
- Exercise 1 (due to 23.10.)
- Exercise 2 (due to 06.11.)
- Exercise 3 (due to 20.11.)
- Exercise 4 (due to 04.12.)
- Exercise 5 (due to 18.12.)
- Exercise 6 (due to 22.01.)
## ResourcesA. 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. Predicate abstraction checks for simple example on the slides in
SMT2 syntax: pred0.smt, pred1.smt, pred2.smt,
pred3.smt, pred4.smt, pred5.smt. All
should be 'sat', except for the last one pred5.smt, where we assume Our award winning SMT solver Boolector. Z3 SMT solver with source code. New genbprbsrch.sh script for generating SMT2 bit-vector formulas for bit-precise reasoning about binary search. 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. See also fast-hash. 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
AIG implementation and visualization: aig4teaching.zip, lg-0.9.tar.gz. BDD implementation and visualization: bdd4teaching.zip, lg-0.9.tar.gz. 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. |