Name
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-39185-9_2 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
single transferable vote,semantic criterion,major international conference,formal method,existing voting scheme,democratic property,bounded model-checking,first-order logic,case study,new voting scheme | Single transferable vote,Model checking,Voting,Computer science,Theoretical computer science,Proportional representation,Formal methods,Semantics,Bounded function,Condorcet method | Conference |
Citations | PageRank | References |
1 | 0.40 | 3 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bernhard Beckert | 1 | 862 | 86.50 |
| Rajeev Goré | 2 | 641 | 63.45 |
| Carsten Schürmann | 3 | 625 | 49.63 |