Automated Verification for Functional and Relational Properties of Voting
Rules
Bernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber, and
Mattias Ulbrich
In this paper, we formalise classes of axiomatic properties for voting rules,
discuss their characteristics, and show how symmetry properties can be
exploited in the verification of other properties. Following that, we describe
how automated verification methods such as software bounded model checking and
deductive verification can be used to verify implementations of voting
rules. We present a case study, where we use and compare dierent approaches
to verify that plurality voting satises the majority and the anonymity
property.