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

[Johannes Hölzl]

** ROOM IS J. v. Neumann MI 00.11.038 **

Dear All,

the Club2 talk will be in 15 min.
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.


_______________________________________________
Club2 mailing list
List page: https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/club2
Webpage with calendar: http://www4.in.tum.de/proj/theoremprov/club2.html