On the Specification and Verification of Voting Schemes

  • Bernhard Beckert
  • Rajeev Goré
  • Carsten Schürmann
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7985)


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.


Vote Scheme Proportional Representation Condorcet Winner Preferential Vote Bound Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Beckert, B., Goré, R., Schürmann, C.: Analysing vote counting algorithms via logic. And its application to the CADE election system. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 135–144. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  2. 2.
    Brams, S., Sanver, R.: Voter sovereignty and election outcomes (2003), (accessed March 21, 2013) (retrieved)
  3. 3.
    Brandt, F., Conitzer, V., Endriss, U.: Computational social choice. In: Weiss, G. (ed.) Multiagent Systems. MIT Press (2012) (forthcoming),
  4. 4.
    CADE Inc.: CADE Bylaws (effective November 1, 1996; amended July/August 2000), (accessed January 20, 2013) (retrieved)
  5. 5.
    Cochran, D.: Formal Specification and Analysis of Danish and Irish Ballot Counting Algorithms. Ph.D. thesis, ITU (2012)Google Scholar
  6. 6.
    Court, F.C.: Provisions of the federal electoral act from which the effect of negative voting weight emerges unconstitutional. Press release no. 68/2008 (2008)Google Scholar
  7. 7.
    Hill, I.D., Wichmann, B.A., Woodall, D.R.: Single transferable vote by Meek’s method. Computer Journal 30(3) (1987)Google Scholar
  8. 8.
    Kiniry, J.R., Cochran, D., Tierney, P.E.: Verification-centric realization of electronic vote counting. Tech. rep., School of Computer Science and Informatics, University College Dublin (2007)Google Scholar
  9. 9.
    McGaley, M., Gibson, J.P.: Electronic voting: A safety critical system. Tech. Rep. NUIM-CS-TR2003-02, Department of Computer Science, National University of Ireland, Maynooth (March 2003)Google Scholar
  10. 10.
    Meskanen, T., Nurmi, H.: Closeness counts in social choice. In: Braham, M., Steffen, F. (eds.) Power, Freedom, and Voting. Springer (2008)Google Scholar
  11. 11.
    Pacuit, E.: Voting methods. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (Winter 2012)Google Scholar
  12. 12.
    Plaisted, D.A.: A consideration of the new cade bylaws, (accessed March 22, 2013) (retrieved)
  13. 13.
    Sun, Y., Zhang, C., Pang, J., Alcalde, B., Mauw, S.: A trust-augmented voting scheme for collaborative privacy management. Journal of Computer Security 20(4), 437–459 (2012)Google Scholar
  14. 14.
    Wikipedia: Monotonicity criterion, (accessed March 21, 2013) (retrieved)
  15. 15.
    Wikipedia: Single transferable vote, (accessed January 20, 2013) (retrieved)

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Bernhard Beckert
    • 1
  • Rajeev Goré
    • 2
  • Carsten Schürmann
    • 3
  1. 1.Karlsruhe Institute of TechnologyGermany
  2. 2.The Australian National UniversityAustralia
  3. 3.IT University of CopenhagenDenmark

Personalised recommendations