KIT | KIT-Bibliothek | Impressum | Datenschutz

An Introduction to Voting Rule Verification

Beckert, Bernhard ORCID iD icon; Bormer, Thorsten; Goré, Rajeev; Kirsten, Michael ORCID iD icon; Schürmann, Carsten


We give an introduction to deductive verification methods that can be used to
formally prove that voting rules and their implementations satisfy specified
properties and conform to the desired democratic principles.

In the first part of the paper we explain the basic principles: We describe
how first-order logic with theories can be used to formalise the desired
properties. We explain the difference between (1) proving that one
set of properties implies another property, (2) proving that a voting rule
implementation has a certain property, and (3) proving that a voting rule
implementation is a refinement of an executable specification. And we explain
the different technologies: (1) SMT-based testing, (2) bounded program
verification, (3) relational program verification, and (4) symmetry breaking.
In this first part of the paper, we also explain the difference between
verifying functional and relational properties (such as symmetries).

In the second part, we present case studies, including (1) the specification
and verification of semantic properties for an STV rule used for electing the
board of trustees for a major international conference and (2) the
... mehr

Verlagsausgabe §
DOI: 10.5445/IR/1000092710
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 Buchaufsatz
Publikationsjahr 2017
Sprache Englisch
Identifikator ISBN: 978-1-32691-209-3
KITopen-ID: 1000092710
Erschienen in Trends in Computational Social Choice. Ed by.: Ulle Endriss
Verlag AI Access
Seiten 269–287
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page