The Distributed Algorithms Working Notation (DAWN) was designed for modeling and veri-fying 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 auto-matically. For each step in a DAWN proof, we can generate a set 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.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.