Model-Checking SS 2012

Model-Checking (also in German: Modellprüfung) is a technique for automatic verification of hardware and software systems. Given a such system and a correctness specification, a model checker checks if the system works correctly.

Prerequisites: Basic discrete math and logic.