### Skapa referens, olika format (klipp och klistra)

**Harvard**

Svensson, H. (2008) *A Semi-Automatic Correctness Proof Procedure applied to Stoller's Leader Election Algorithm*. Göteborg : Chalmers University of Technology (Technical report - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, nr: 2008:7).

** BibTeX **

@techreport{

Svensson2008,

author={Svensson, Hans},

title={A Semi-Automatic Correctness Proof Procedure applied to Stoller's Leader Election Algorithm},

abstract={In 1997, Stoller presented a leader election algorithm for a synchronous system with crash failures. The algorithm is an adaptation of Garcia-Molina's Bully Algorithm that uses failure detectors instead of explicit timeouts. Since the characteristics of the algorithm closely resemble the Bully Algorithm Stoller does not give a formal correctness proof. However, although the algorithms appear similar, there are non-trivial differences. The differences make it unclear if the original proof, by Garcia-Molina, actually carries over as indicated by Stoller. In this document we formalize the leader election algorithm using first-order logic, and prove its correctness with respect to the obvious safety property; it should not be possible to elect two different leaders at the same time.},

publisher={Chalmers University of Technology},

place={Göteborg},

year={2008},

series={Technical report - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, no: 2008:7},

note={22},

}

** RefWorks **

RT Report

SR Print

ID 69237

A1 Svensson, Hans

T1 A Semi-Automatic Correctness Proof Procedure applied to Stoller's Leader Election Algorithm

YR 2008

AB In 1997, Stoller presented a leader election algorithm for a synchronous system with crash failures. The algorithm is an adaptation of Garcia-Molina's Bully Algorithm that uses failure detectors instead of explicit timeouts. Since the characteristics of the algorithm closely resemble the Bully Algorithm Stoller does not give a formal correctness proof. However, although the algorithms appear similar, there are non-trivial differences. The differences make it unclear if the original proof, by Garcia-Molina, actually carries over as indicated by Stoller. In this document we formalize the leader election algorithm using first-order logic, and prove its correctness with respect to the obvious safety property; it should not be possible to elect two different leaders at the same time.

PB Chalmers University of Technology

T3 Technical report - Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, no: 2008:7

LA eng

OL 30