Automated Verification for Functional and Relational Properties of Voting Rules

Reviewed Paper In Proceedings

Author(s):Bernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber, and Mattias Ulbrich
In:Sixth International Workshop on Computational Social Choice (COMSOC 2016)
Year:2016
URL:https://www.irit.fr/COMSOC-2016/proceedings/BeckertEtAlCOMSOC2016.pdf

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.

BibTeX

@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.},
  place			= {Toulouse, France},
  date			= {June 22-24}
}