TNF / INF

team
contact
software
publications
teaching
jobs

Model Checking

Winter Semester 2020

Armin Biere, Nils Froleyks

Schedule

Lecture: Thursdays, 8:30 - 10:00, Cyberspace. For more information see the Moodle course.

Overview

This lecture is a course in the Computer Science Master.

Teaching language is English.

Slides

Here you find the latest version 2020.1 of the slides:

[ mcslides.pdf ]

We are going to update slides during the semester. The slide set is not considered to be complete before the end of the semester.

Exercises

The exercises will be organized through Moodle.

Resources

Most relevant for this lectures are the following chapters

of the Handbook of Model Checking, Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem editors, Springer 2018.

Model Checking (2nd edition). E. Clarke, O. Grumberg, D. Kröning, D. Peled, H. Veith. MIT press, 2018.

McRaceTrack model checker published.

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.

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 i != INT_MAX. The check pred2.smt actually shows, that we would need "b = *;" instead of "if (b) b = *;" if we consider bit-precise reasoning (so 32 bit 2-complement int and not integers).

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, such as this one bprsrch01p1oan.smt2.

The McRaceTrack model checker is used to explain and motivate the part on explicit state model checking.

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 (1st edition). 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 Proc. 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'06), Mikulov, Czechia, October 2006.

AIG implementation and visualization: aig4teaching.zip, requires dot and evince for visualization.

BDD implementation and visualization: bdd4teaching.zip, requires dot and evince for visualization.

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.