Why3-do: The Way of Harmonious Distributed System Proofs

Abstract

Abstract We study principles and models for reasoning inductively about properties of distributed systems, based on programmed atomic handlers equipped with contracts. We present the Why3-do library, leveraging a state of the art software verifier for reasoning about distributed systems based on our models. A number of examples involving invariants containing existential and nested quantifiers (including Dijsktra’s self-stabilizing systems) illustrate how the library promotes contract-based modular development, abstraction barriers, and automated proofs.