On the Specification and Verification of Voting Schemes

@inproceedings{BeckertGoreSchuermann2013b,
  author    = {Bernhard Beckert and Rajeev Gor\'e and Carsten Sch\"urmann},
  title     = {On the Specification and Verification of Voting Schemes},
  pages     = {25--40},
  doi       = {10.1007/978-3-642-39185-9_2},
  booktitle = {4th International Conference on E-Voting and Identity (Vote-ID 2013)},
  editor    = {James Heather and Steve A. Schneider and Vanessa Teague},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {7985},
  year      = {2013},
  month     = jul,
  eventdate = {2013-07-17/2013-07-19},
  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.},
  venue     = {Guildford, UK}
}