Model Checking

What it is about

You will learn how to describe hardware and software systems with formal models and how to automatically verify these models using model checking methods to determine whether they satisfy desired properties. In the end you will be able to model simple systems, formulate properties in temporal logic, and explain basic model-checking algorithms as well as strategies against the state-space explosion problem and apply them to small examples.

What you will be able to do

• Explain the role of model checking for software and hardware quality
• Specify formal models of simple systems
• Formulate safety and liveness properties in temporal logic
• Apply algorithms for checking specifications
• Explain techniques to contain the state-space problem

What the module consists of

• VorlesungConveying the fundamentals, introducing techniques and tools; during lectures small exercises are solved online
• Tutorium/ÜbungDiscussion and deepening of the weekly problem solutions

Teaching method

• VorlesungIntroduction to theory, methods and tools; interactive online exercises for deepening
• TutoriumDiscussion and review of the weekly tasks
• schriftliche AufgabenRegular exercises for practical application and exam preparation
• Tool-DemonstrationenHands-on experience using model-checking tools such as Spin, Blast, CBMC