Serviceverbund KIM

Streaming Server

Login |
 
 

Model Checking of Software and Systems

Dozenten

Prof. Dr. Stefan Leue

Alina Bey, Mitra Tabaei

Termine (Vorlesung)

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

Inhalt

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.

RSS-Feed

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

RSS LogoRSS-Feed abonnieren

Episoden

Öffnet internen Link im aktuellen Fenster2011/04/13 (Mi) - IntroductionINF-12020-20111_2011-04-12_01

Öffnet internen Link im aktuellen Fenster2011/04/14 (Do) - Systems and Software Failures

Öffnet internen Link im aktuellen Fenster2011/04/20 (Mi) - Model Checking in the Software Process

Öffnet internen Link im aktuellen Fenster2011/04/20 (Mi) - State-based modelling using Promela & SPIN

Öffnet internen Link im aktuellen Fenster2011/04/21 (Do) - NO LECTURE (Easter Holidays)

Öffnet internen Link im aktuellen Fenster2011/04/27 (Mi) - (Part II) State-based modelling using Promela & SPIN

Öffnet internen Link im aktuellen Fenster2011/04/28 (Do) - (Part III) State-based modelling using Promela & SPININF-12110-20111_2011-05-04_01

Öffnet internen Link im aktuellen Fenster2011/05/04 (Mi) - Transition SystemsINF-12110-20111_2011-04-28-02

Öffnet internen Link im aktuellen Fenster2011/05/05 (Do) - Transition Systems Part II

Öffnet internen Link im aktuellen Fenster2011/05/11 (Mi) - Modeling Concurrency

Öffnet internen Link im aktuellen Fenster2011/05/12 (Do) - Channel Systems

Öffnet internen Link im aktuellen Fenster2011/05/18 (Mi) - State Machine Models

INF-12110-20111_2011-05-19_01Öffnet internen Link im aktuellen Fenster2011/05/19 (Do) - Linear-Time Properties and Invariants

Öffnet internen Link im aktuellen Fenster2011/05/25 (Mi) - Safety and Liveness

Öffnet internen Link im aktuellen Fenster2011/05/26 (Do) - Safety and Liveness II

Öffnet internen Link im aktuellen Fenster2011/06/01 (Mi) - Fairness

Öffnet internen Link im aktuellen Fenster2011/06/02 (Do) - NO LECTURE (Holidays)

Öffnet internen Link im aktuellen Fenster2011/06/08 (Mi) - Omega-Regular Languages

Öffnet internen Link im aktuellen Fenster2011/06/09 (Do) - Nondeterministic Finite Büchi Automata (NBA)

Öffnet internen Link im aktuellen Fenster2011/06/22 (Mi) - LTL and Büchi Automata

Öffnet internen Link im aktuellen Fenster2011/06/23 (Do) - NO LECTURE (Holidays)

Öffnet internen Link im aktuellen Fenster2011/06/29 (Mi) - Algorithms for Checking Safety Properties

Öffnet internen Link im aktuellen Fenster2011/06/30 (Do) - Model Checking of Omega-Regular Properties

Öffnet internen Link im aktuellen Fenster2011/07/06 (Mi) - Partial Order Reduction

Öffnet internen Link im aktuellen Fenster2011/07/07 (Do) - Partial Order Reduction, Part II