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, we present recent work on verification techniques for
distributed systems that are automatic and "as complete as possible", or
complete and "as automatic as possible". We illustrate our work with the
analysis of Chord, a scalable distributed hash table.