On the Specification and Verification of Voting Schemes
Bernhard Beckert, Rajeev Gore, and Carsten Schürmann
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.