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:
Episoden
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/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