PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

ILF and DAWN for verifying distributed algorithms : an idea for a tool

Autorzy
Wybrane pełne teksty z tego czasopisma
Identyfikatory
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
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.
Wydawca
Rocznik
Strony
201--211
Opis fizyczny
bibliogr. 16 poz.
Twórcy
autor
autor
Bibliografia
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-article-BUS1-0007-0013
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ć.