Verifying Voting Schemes

@article{BeckertGoreSchuermannEA2014,
  title      = {Verifying Voting Schemes},
  author     = {Bernhard Beckert and Rajeev Gor\'e and Carsten Sch\"urmann and 
                Thorsten Bormer and Jian Wang},
  journal    = {Journal of Information Security and Applications (JISA)},
  volume     = {19},
  number     = {2},
  pages      = {115--129},
  ISSN       = {2214-2126},
  year       = {2014},
  month      = apr,
  doi        = {10.1016/j.jisa.2014.04.005},
  abstract   = {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 define 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 interna-
  		tional conference and discuss its deficiencies.}
}