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.

@InCollection{beckertBormerGoreEA2017,
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/}
}