Proving distributed hylomorphisms

Abstract

This report presents detailed formal proofs of the correctness of distributed hylomorphisms with respect to their termination. The main objectives of the verification strategy are (a) to reduce proof effort and complexity by using the refinements framework from [VS01] and re-using as many results as possible, and (b) to write (or represent) comprehensible proofs by incrementally constructing invariants that are not pulled out of a hat.