[Club2] Talk by Johannes Hölzl -- Thu. Aug 23, 2 PM, J.v Neumann (MI 00.11.038)

[Johannes Hölzl]

Dear All,

this week the Club2 talk will not be today but tomorrow.
I will give my rehearsal talk for the QFM2012 on Tuesday in Paris.

Best regards,
  Johannes

Interactive verification of Markov chains: Two distributed protocol case studies
Johannes Hölzl and Tobias Nipkow
==========================================
Thu. Aug 23, 2 PM, J.v Neumann (MI 00.11.038)

Probabilistic model checkers like PRISM only check probabilistic systems
of a fixed size. To guarantee the desired properties for an arbitrary
size, mathematical analysis is necessary. We show for two case studies
how this can be done in the interactive proof assistant Isabelle/HOL.
The first case study is a detailed description of how we verified
properties of the ZeroConf protocol, a decentral address allocation
protocol. The second case study shows the more involved verification of
anonymity properties of the Crowds protocol, an anonymizing protocol.