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

• Autorzy: Baar T. , Kindler E.
• 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.

Słowa kluczowe

EN

automated theorem provers; distributed algorithms; verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 1999
• Tom: Vol. 37, Nr 3
• Strony: 201--211
• Opis fizyczny: bibliogr. 16 poz.

Twórcy

autor

Baar T.

autor

Kindler E.

• Institut für Informatik Humboldt-Universität zu Berlin D-10099 Berlin, Germany,