An Introduction to Voting Rule Verification

Buchkapitel

Autor(en):Bernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten und Carsten Schürmann
In:Trends in Computational Social Choice
Verleger:AI Access
Teil:II: Techniques
Kapitel:14
Jahr:2017
Seiten:269-287
PDF:
URL:http://research.illc.uva.nl/COST-IC1205/Book/
Links:

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.
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).
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.

BibTeX

@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       = {http://research.illc.uva.nl/COST-IC1205/Book/}
}