On the specification and verification of voting schemes

Bernhard Beckert; Rajeev Goré; Carsten Schürmann

doi:10.1007/978-3-642-39185-9_2

On the specification and verification of voting schemes

Bernhard Beckert, Rajeev Goré, Carsten Schürmann

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Citation (Scopus)

Abstract

The ability to count ballots by computers allows us to design new voting schemes that are arguably fairer than existing schemes designed for hand-counting. We argue that formal methods can and should be used to ensure that such schemes behave as intended and are conform to the desired democratic properties. Specifically, we define two semantic criteria for single transferable vote (STV) schemes, formulated in first-order logic, and show how bounded model-checking can be used to test whether these criteria are met. As a case study, we then analyse an existing voting scheme for electing the board of trustees for a major international conference and discuss its deficiencies.

Original language	English
Title of host publication	E-Voting and Identity - 4th International Conference, Vote-ID 2013, Proceedings
Pages	25-40
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-39185-9_2
Publication status	Published - 2013
Event	4th International Conference on E-Voting and Identity, Vote-ID 2013 - Guildford, United Kingdom Duration: 17 Jul 2013 → 19 Jul 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7985 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	4th International Conference on E-Voting and Identity, Vote-ID 2013
Country/Territory	United Kingdom
City	Guildford
Period	17/07/13 → 19/07/13

Access to Document

10.1007/978-3-642-39185-9_2

Cite this

Beckert, B., Goré, R., & Schürmann, C. (2013). On the specification and verification of voting schemes. In E-Voting and Identity - 4th International Conference, Vote-ID 2013, Proceedings (pp. 25-40). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7985 LNCS). https://doi.org/10.1007/978-3-642-39185-9_2

@inproceedings{a1bf0b53bc504e84847ea0cd1b2c6806,

title = "On the specification and verification of voting schemes",

abstract = "The ability to count ballots by computers allows us to design new voting schemes that are arguably fairer than existing schemes designed for hand-counting. We argue that formal methods can and should be used to ensure that such schemes behave as intended and are conform to the desired democratic properties. Specifically, we define two semantic criteria for single transferable vote (STV) schemes, formulated in first-order logic, and show how bounded model-checking can be used to test whether these criteria are met. As a case study, we then analyse an existing voting scheme for electing the board of trustees for a major international conference and discuss its deficiencies.",

author = "Bernhard Beckert and Rajeev Gor{\'e} and Carsten Sch{\"u}rmann",

year = "2013",

doi = "10.1007/978-3-642-39185-9_2",

language = "English",

isbn = "9783642391842",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "25--40",

booktitle = "E-Voting and Identity - 4th International Conference, Vote-ID 2013, Proceedings",

note = "4th International Conference on E-Voting and Identity, Vote-ID 2013 ; Conference date: 17-07-2013 Through 19-07-2013",

}

Beckert, B, Goré, R & Schürmann, C 2013, On the specification and verification of voting schemes. in E-Voting and Identity - 4th International Conference, Vote-ID 2013, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7985 LNCS, pp. 25-40, 4th International Conference on E-Voting and Identity, Vote-ID 2013, Guildford, United Kingdom, 17/07/13. https://doi.org/10.1007/978-3-642-39185-9_2

On the specification and verification of voting schemes. / Beckert, Bernhard; Goré, Rajeev; Schürmann, Carsten.
E-Voting and Identity - 4th International Conference, Vote-ID 2013, Proceedings. 2013. p. 25-40 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7985 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - On the specification and verification of voting schemes

AU - Beckert, Bernhard

AU - Goré, Rajeev

AU - Schürmann, Carsten

PY - 2013

Y1 - 2013

N2 - The ability to count ballots by computers allows us to design new voting schemes that are arguably fairer than existing schemes designed for hand-counting. We argue that formal methods can and should be used to ensure that such schemes behave as intended and are conform to the desired democratic properties. Specifically, we define two semantic criteria for single transferable vote (STV) schemes, formulated in first-order logic, and show how bounded model-checking can be used to test whether these criteria are met. As a case study, we then analyse an existing voting scheme for electing the board of trustees for a major international conference and discuss its deficiencies.

AB - The ability to count ballots by computers allows us to design new voting schemes that are arguably fairer than existing schemes designed for hand-counting. We argue that formal methods can and should be used to ensure that such schemes behave as intended and are conform to the desired democratic properties. Specifically, we define two semantic criteria for single transferable vote (STV) schemes, formulated in first-order logic, and show how bounded model-checking can be used to test whether these criteria are met. As a case study, we then analyse an existing voting scheme for electing the board of trustees for a major international conference and discuss its deficiencies.

UR - http://www.scopus.com/inward/record.url?scp=84880890582&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-39185-9_2

DO - 10.1007/978-3-642-39185-9_2

M3 - Conference contribution

SN - 9783642391842

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 25

EP - 40

BT - E-Voting and Identity - 4th International Conference, Vote-ID 2013, Proceedings

T2 - 4th International Conference on E-Voting and Identity, Vote-ID 2013

Y2 - 17 July 2013 through 19 July 2013

ER -

On the specification and verification of voting schemes

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this