Model Checking of Software and Systems


Prof. Dr. Stefan Leue

Alina Bey, Mitra Tabaei

Termine (Vorlesung)

Mi 10:00 - 12:00 C252
Do 10:00 - 12:00 C252


The course will introduce into explicit state model checking for reactive software systems. Model checking is an algorithmic, automated technique for the behavioral analysis of soft- and hardware systems. We will illustrate the algorithmic foundations of this technique, present the SPIN tool, and address advanced topics. The accompanying project will address the modeling and analysis of an industrial case-study. Participants are expected to possess a basic knowledge in programming, concurrent systems, automata theory and logic.

Further Details and information on the accompanying website.


Um automatisch benachrichtigt zu werden sobald eine neue Episode online ist:

RSS-Feed abonnieren


2011/04/13 (Mi) - Introduction

2011/04/14 (Do) - Systems and Software Failures

2011/04/20 (Mi) - Model Checking in the Software Process

2011/04/20 (Mi) - State-based modelling using Promela & SPIN

2011/04/21 (Do) - NO LECTURE (Easter Holidays)

2011/04/27 (Mi) - (Part II) State-based modelling using Promela & SPIN

 2011/04/28 (Do) - (Part III) State-based modelling using Promela & SPIN

2011/05/04 (Mi) - Transition Systems

2011/05/05 (Do) - Transition Systems Part II

2011/05/11 (Mi) - Modeling Concurrency

2011/05/12 (Do) - Channel Systems

2011/05/18 (Mi) - State Machine Models

 2011/05/19 (Do) - Linear-Time Properties and Invariants

2011/05/25 (Mi) - Safety and Liveness

2011/05/26 (Do) - Safety and Liveness II

2011/06/01 (Mi) - Fairness

2011/06/02 (Do) - NO LECTURE (Holidays)

2011/06/08 (Mi) - Omega-Regular Languages

2011/06/09 (Do) - Nondeterministic Finite Büchi Automata (NBA)

2011/06/22 (Mi) - LTL and Büchi Automata

2011/06/23 (Do) - NO LECTURE (Holidays)

2011/06/29 (Mi) - Algorithms for Checking Safety Properties

2011/06/30 (Do) - Model Checking of Omega-Regular Properties

2011/07/06 (Mi) - Partial Order Reduction

2011/07/07 (Do) - Partial Order Reduction, Part II