An Introduction to Voting Rule Verification

@InCollection{BeckertBormerEA2017,
  author    = {Bernhard Beckert and Thorsten Bormer and
	       Rajeev Gor\'e and Michael Kirsten and
	       Carsten Sch\"urmann},
  title     = {An Introduction to Voting Rule Verification},
  booktitle = {Trends in Computational Social Choice},
  chapter   = {14},
  part      = {II: Techniques},
  pages     = {269--287},
  year      = {2017},
  abstract  = {We give an introduction to deductive verification methods that can be used to
	       formally prove that voting rules and their implementations satisfy specified
	       properties and conform to the desired democratic principles.
	       \newline

	       In the first part of the paper we explain the basic principles: We describe
	       how first-order logic with theories can be used to formalise the desired
	       properties. We explain the difference between (1) proving that one
	       set of properties implies another property, (2) proving that a voting rule
	       implementation has a certain property, and (3) proving that a voting rule
	       implementation is a refinement of an executable specification. And we explain
	       the different technologies: (1) SMT-based testing, (2) bounded program
	       verification, (3) relational program verification, and (4) symmetry breaking.
	       In this first part of the paper, we also explain the difference between
	       verifying functional and relational properties (such as symmetries).
	       \newline

	       In the second part, we present case studies, including (1) the specification
	       and verification of semantic properties for an STV rule used for electing the
	       board of trustees for a major international conference and (2) the
	       deduction-based computation of election margins for the Danish national
	       parliamentary elections.},
  month     = oct,
  editor    = {Ulle Endriss},
  publisher = {AI Access},
  url       = {https://research.illc.uva.nl/COST-IC1205/Book/}
}