Julien Brunel and David Chemouil are senior researchers at ONERA, in Toulouse, specialized in formal specification and verification. Together with Nuno Macedo and Alcino Cunha (INESC TEC) they designed the 6th version (dubbed Electrum until recently) of the Alloy language and tool (originally proposed by the MIT). In recent years, Julien Brunel and David Chemouil have also been studying the verification of distributed algorithms. A recent highlight is the first mechanical proof of correctness of the distributed maintenance algorithm of the Chord peer-to-peer protocol, as well as formal techniques for the complete, semi-automatic verification of infinite-state systems, such as distributed algorithms.
Join us on the 8th April, at 14:30, in room I-105 of FEUP, for the presentation of this work.
Abstract:
The verification of distributed systems is challenging because these systems combine a rich structure, a high number of elements and a non-trivial temporal evolution. A trade-off between automation and completeness of the verification has to be made. In particular, one can use theorem provers, which offer complete confidence but tend to require considerable expertise and effort. Another option is to use model checkers, which offer complete automation, but cannot handle complex data structures and configurations.
In this talk, they will present recent work on verification techniques for distributed systems that are automatic and “as complete as possible”, or complete and “as automatic as possible”. They will illustrate their work with the analysis of Chord, a scalable distributed hash table.