KIT | KIT-Bibliothek | Impressum | Datenschutz

Formal Verification of Voting Schemes

Kirsten, Michael

Abstract:
Fundamental trust and credibility in democratic systems is commonly established through
the existence and execution of democratic elections. The vote-counting of an election,
usually formalised by a voting scheme, essentially boils down to a mechanism that
aggregates individual preferences of the voters to reach a decision. For this matter, there
are various differing voting schemes in use throughout the world, commonly based on
high expectations and means to ensure a sensible democratic process. However, incidents
such as the ruling by the German federal constitutional court which led to a change of
the German legislation in 2013 manifest that it is difficult for a voting scheme to meet
these legitimate expectations. In fact, there is no general notion of correctness
for a voting scheme and thus no universal mechanism as shown in Kenneth J. Arrow’s
Impossibility Theorem in 1951. As a consequence, designing a real-world voting
scheme without flaws, which still gives significant democratic guarantees, is a difficult
task as a trade-off between desirable properties is non-trivial and error-prone.

The approach in this thesis is based on the idea to tackle this issue by proposing an
incremental and iterative development process for voting schemes based on automated
formal reasoning methods using program verification. ... mehr

Open Access Logo


Volltext §
DOI: 10.5445/IR/1000092716
Veröffentlicht am 28.03.2019
Coverbild
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Hochschulschrift
Jahr 2014
Sprache Englisch
Identifikator urn:nbn:de:swb:90-927160
KITopen-ID: 1000092716
Verlag KIT, Karlsruhe
Umfang 129 S.
Abschlussart Abschlussarbeit - Diplom
Schlagworte software software engineering requirements/specifications software/program verification
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page