QUANTITATIVE MODEL CHECKING
This advanced course addresses Bachelor and Master students in Computer Science, Bioinformatics, CuK or Computerlinguistics. Background in probability theory and the module Verification are of advantage but not mandatory.
Quatitative model checking is an approach for verifying systems exibihting random phenomena. Such systems include networked, embedded, and more recently biological systems. They have usually discrete-time and/or continuous-time Markov chains, together with their extensions with nondeterminism, as their underlying semantics. With quatitative model checking technique properties of interest can be verified against the respective models. The properties can be specified by PCTL, LTL, PCTL* for discrete-time models, and CSL for continuous-time models. This course aims to cover both the model construction and the verification techniques for these systems.
Dates and Venue
The course starts on April 14, 2010 and spans the summer term 2010.
Lectures take place each Wednesday at 08:30-10:00, in E1 3 - HS 1.
Tutorials timeslots are Fridays 12:30-14:00, starting April 23.
Further details are available at the CMS.
|Dependable Systems & Software Group||Department of Computer Science||Universität des Saarlandes|