Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Compositional Verification of Social Choice Properties for Single Transferable Vote Using an Interactive Theorem Prover

Forschungsthema:Computational Social Choice
Typ: BA
Datum: 2021-02-01
Betreuer: Michael Kirsten
Aushang:

Abstract

Decisions need to be made in many situations, both for high-stakes occasions such as presidential or parliamentary elections, for boards of trustees, but also in low-stakes every life such as deciding which restaurant to go to as a group of friends. A famous method in the case of elections is the Single Transferable Vote (STV) which allows to rank candidates by preference. STV then iteratively eliminates options with the least amount of top preferences by transfering their votes to the next preferred option until a clear winner is found, however throughout the world different variants of STV are in use.
Within this thesis, we want to prove interesting fairness properties such as the clone-proofness property for selected variants of STV. As STV is rather complex and has many variants, we want to decompose STV into smaller manageable parts using a modular composition framework verified within the interactive theorem prover Isabelle/HOL. By this, we want to flexibly parameterize and compose general variants of STV together with correct-by-construction proofs that the properties of interest are satisfied.

Literature