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 Locations
The course spans the winter term 2013/14.
The first meeting will take place in 401, E 1.3 on 17/10/2013, Thursday, 4PM-5:30PM.
The second lecture at 2PM-4PM, Tuesday, Oct 22, 2013 will take place in E2.5 SR 4 (U.16).
All remaining lectures will take place in 528, E1.3, Tuesday, 2PM-4PM.
Tutorials will take place in 528, E1.3, Tuesday, 10AM-12PM.
For those who cannot make it, you can find us in 534, E1.3, Monday, 10AM-12PM.
Final written Exam will take place in E1.3, 528, on Tue, February 18, 2014, 2pm – 4pm (90min).
In order to participate the final exam, you need to get at least 50% points for both theoretical and practical exercises. You can ask Hassan for your latest points.
Principles of Model Checking. Christel Baier and Joost-Pieter Katoen, MIT Press, 2008.
Slides may be updated constantly due to typos.
You can work in group of at most 2 people.
For the practical exercise, please send your implementation to Hassan by email,
with name "XXYY.tgz", where "XX" is your last name and "YY" the number of the practical exercise, for instance "song01.tgz".
(Deadline Extended) All practical exercises handed in before 23:59, Feb. 4th, 2014 will be counted.
|Dependable Systems & Software Group||Department of Computer Science||Universität des Saarlandes|