ILF and DAWN for Verifying Distributed Algorithms – An Idea for a Tool

Abstract

The Distributed Algorithms Working Notation (DAWN) was designed for modelling and verifying algorithms in an intuitive way. Nevertheless, DAWN proofs are formal. In this paper, we show that it is possible to check correctness of a DAWN proof fully automatically: For each step in a DAWN proof, we can generate a set of proof obligations which can automatically be checked by help of automated theorem provers. The verification tool ILF provides a uniform interface to many theorem provers—which makes it an ideal partner for DAWN and a basis for building a DAWN-tool.