An Introduction to Voting Rule Verification

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
... mehr
deduction-based computation of election margins for the Danish national
parliamentary elections.