Abstract
Vote counting schemes, in particular those that employ various different variants of single transferable vote, often vary in small details. How are transfer values computed? What are the precise rules when two or more candidates tie for exclusion? In what order are candidates elected? these details are crucial for the correctness of vote counting software. While the verification of counting programs using interactive theorem provers gives very high correctness guarantees, correctness proofs need to be re-done, as both specification and implementation change. This paper presents a framework where counting schemes are specified by rules, and provably correct, universally verifiable counting programs can be synthesised automatically, given (formal) proofs of two simple and intuitive properties of the specification of the protocol in rule form.
| Original language | English |
|---|---|
| Title of host publication | Modular Synthesis of Provably Correct Vote Counting Programs |
| Editors | R Krimmer, M Volkamer, J Barrat, J Benaloh, N Goodman, P Ryan and V Teague |
| Place of Publication | Switzerland |
| Publisher | Springer International Publishing AG |
| Pages | 55-70pp |
| Edition | Peer reviewed |
| ISBN (Print) | 9783319522401 |
| Publication status | Published - 2016 |
| Event | 1st International Joint Conference on Electronic Voting, E-Vote-ID 2016 - Bregenz, Austria Duration: 1 Jan 2016 → … |
Conference
| Conference | 1st International Joint Conference on Electronic Voting, E-Vote-ID 2016 |
|---|---|
| Period | 1/01/16 → … |
| Other | October 18-21 2016 |