Automated Verification for Functional and Relational Properties of Voting Rules

@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},
  editor                = {Umberto Grandi and
                           Jeffrey S. Rosenschein},
  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}
}