[Club2] Talk by Giuliano Losa: Friday, August 30, 10:00, Room Turing (00.09.38)

[Andrei Popescu]

Dear All,  

The coming Friday we have a talk by Giuliano Losa.  
Giuliano is working with Viktor Kuncak on the verification of distributed algorithms.  

Cheers, 
 Andrei 

Giuliano Losa -- Reasoning about adaptive distributed algorithms
================================================================
Friday, August 30, 10:00, Room Turing (00.09.38)

To reach practical performance, distributed algorithm must dynamically
adapt to their environment (faults, asynchrony, load, contention...).
Adaptive distributed algorithms often achieve dynamic adaptation by
switching between several modes, each mode being a complex algorithm on
its own. The interaction between modes presents a challenge to formal
verification. Indeed, we do not know of any formally verified adaptive
distributed algorithm.
We present a framework in which each mode of an adaptive distributed
algorithm can be specified and verified independently of the other
modes. We demonstrate that our framework enables verifying adaptive
distributed algorithms using several examples formalized in TLA and
Isabelle/HOL.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20130824/7dca2f5a/attachment.html>