Verifying Voting Schemes
Bernhard Beckert, Rajeev Goré, Carsten Schürmann, Thorsten Bormer, and Jian Wang
The possibility to use computers for counting ballots 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
conform to the desired democratic properties. Specifically, we dene
two semantic criteria for single transferable vote (STV) schemes,
formulated in first-order logic over the theories of arrays and
integers, and show how bounded model-checking and SMT solvers can be
used to check 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.