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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Brams, S., Sanver, R.: Voter sovereignty and election outcomes (2003), http://www.nyu.edu/gsas/dept/politics/faculty/brams/sovereignty.pdf (accessed March 21, 2013) (retrieved)
Brandt, F., Conitzer, V., Endriss, U.: Computational social choice. In: Weiss, G. (ed.) Multiagent Systems. MIT Press (2012) (forthcoming), http://www.illc.uva.nl/~ulle/pubs/files/BrandtEtAlMAS2012.pdf
CADE Inc.: CADE Bylaws (effective November 1, 1996; amended July/August 2000), http://www.cadeinc.org/Bylaws.html (accessed January 20, 2013) (retrieved)
Cochran, D.: Formal Specification and Analysis of Danish and Irish Ballot Counting Algorithms. Ph.D. thesis, ITU (2012)
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)
Hill, I.D., Wichmann, B.A., Woodall, D.R.: Single transferable vote by Meek’s method. Computer Journal 30(3) (1987)
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)
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)
Meskanen, T., Nurmi, H.: Closeness counts in social choice. In: Braham, M., Steffen, F. (eds.) Power, Freedom, and Voting. Springer (2008)
Pacuit, E.: Voting methods. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (Winter 2012)
Plaisted, D.A.: A consideration of the new cade bylaws, http://www.cs.unc.edu/Research/mi/consideration.html (accessed March 22, 2013) (retrieved)
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)
Wikipedia: Monotonicity criterion, http://en.wikipedia.org/wiki/Monotonicity_criterion (accessed March 21, 2013) (retrieved)
Wikipedia: Single transferable vote, http://en.wikipedia.org/wiki/Single_transferable_vote (accessed January 20, 2013) (retrieved)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beckert, B., Goré, R., Schürmann, C. (2013). On the Specification and Verification of Voting Schemes. In: Heather, J., Schneider, S., Teague, V. (eds) E-Voting and Identify. Vote-ID 2013. Lecture Notes in Computer Science, vol 7985. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39185-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-39185-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39184-2
Online ISBN: 978-3-642-39185-9
eBook Packages: Computer ScienceComputer Science (R0)