KIT | KIT-Bibliothek | Impressum | Datenschutz

Automated Verification for Functional and Relational Properties of Voting Rules

Beckert, Bernhard ORCID iD icon; Bormer, Thorsten; Kirsten, Michael ORCID iD icon; Neuber, Till; Ulbrich, Mattias ORCID iD icon


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.

Postprint §
DOI: 10.5445/IR/1000092712
Veröffentlicht am 28.03.2019
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2016
Sprache Englisch
Identifikator urn:nbn:de:swb:90-927122
KITopen-ID: 1000092712
Erschienen in Sixth International Workshop on Computational Social Choice, COMSOC-2016, Toulouse, France, 22–24 June 2016
Veranstaltung 6th International Workshop on Computational Social Choice (2016), Toulouse, Frankreich, 22.06.2016 – 24.06.2016
Seiten 16 S.
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page