Quantitative Verification - Summer Term 2019

Traditional functional verification ("The system will always reach a safe state") often provides unsatisfactory results: If messages are transmitted via an unreliable connection, single pakets can get lost, no matter how often transmission is repeated; for each flight on a plane, there is always a larger-than-zero probability of a critical event happening. Therefor, traditional verification would classify both systems as unsafe.
However, there is a clear difference between a critical situation happening with a probability of 10^-2 or 10^-10. In the former case, you’d rather not board the plane, but in the latter, the risk is very manageable.

The goal of the lecture "Quantitative Verification" is to develop models and algorithms that allow for the quantitative analysis of safety properties and to compute cost measurements ("How long will it take on average to transmit to message?").