@InProceedings{BeckertBormerEA2016,
title = {Automated Verification for Functional and Relational
Properties of Voting Rules},
author = {Bernhard Beckert and Thorsten Bormer
and Michael Kirsten and Till Neuber
and Mattias Ulbrich},
booktitle = {Sixth International Workshop on Computational Social Choice (COMSOC 2016)},
url = {https://www.irit.fr/COMSOC-2016/proceedings/BeckertEtAlCOMSOC2016.pdf},
month = jun,
year = {2016},
abstract = {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 different approaches to verify that
plurality voting satisfies the majority and the anonymity property.},
venue = {Toulouse, France},
eventdate = {2016-06-22/2016-06-24},
%% SNIP
keywords = {COMSOC}
}