Affiliations: Institut für Informatik, Humboldt-Universität zu Berlin, D-10099 Berlin, Germany. [email protected] | Institut für Informatik, Humboldt-Universität zu Berlin, D-10099 Berlin, Germany. [email protected]
Note: [] Supported by the DFG: Project ‘Deduktion für Fremdnutzer' within the ‘Schwerpunktprogramm Deduktion'.
Note: [] Address for correspondence: Institut für Informatik, Humboldt-Universität zu Berlin, D-10099 Berlin, Germany Supported by the DFG: Projects ‘Petri Net Technology' and ‘Datenkonsistenzkriterien'.
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.
Keywords: Automated Theorem Provers, Distributed Algorithms, Verification, Z
