Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A Proof of a Leader Election Protocol in microCRL ($\mu$CRL)
RISE - Research Institutes of Sweden, ICT, SICS.
1995 (English)Report (Other academic)
Abstract [en]

In 1982 Dolev, Klawe & Rodeh presented an O(n log n) unidirectional distributed algorithm for the circular extrema-finding (or leader-election) problem}. At the same time Peterson came up with a nearly identical solution. In this paper, we bring the correctness of this algorithm to a completely formal level. This relatively small protocol, which can be described on half a page, requires a rather involved proof for guaranteeing that it behaves well in all possible circumstances. To our knowledge, this is one of the more advanced case-studies in formal verification based on process algebra.

Place, publisher, year, edition, pages
Swedish Institute of Computer Science , 1995, 1. , p. 24
Series
SICS Research Report, ISSN 0283-3638 ; R95:01
Keywords [en]
Formal Methods, Process algebra, Protocol verification
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:ri:diva-21393OAI: oai:DiVA.org:ri-21393DiVA, id: diva2:1041429
Available from: 2016-10-31 Created: 2016-10-31 Last updated: 2018-02-02Bibliographically approved

Open Access in DiVA

fulltext(2030 kB)0 downloads
File information
File name FULLTEXT01.pdfFile size 2030 kBChecksum SHA-512
ec8cf20d27f203e0f862fb66828fb635d738e94e292eac920a13d1df693fc3d58b266b1a0c172bc333b22d6c8370e3ab8d9b7179b7a9fff86adbf8f68982aa36
Type fulltextMimetype application/pdf

By organisation
SICS
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 4 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
v. 2.35.2