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 di erent approaches to verify that plurality voting satis es the majority and the anonymity property.