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

Judging in Competitive Dancing: Formal Verification of the Skating System

Forschungsthema:Computational Social Choice
Typ: BA
Datum: 2023-09-21
Betreuer: Michael Kirsten
Aushang:

Abstract

Voting rules are mathematical functions which evaluate a candidate pool and associated votes to elect one or more candidates in an election. Within previous work at KIT, a framework in the proof-assistant Isabelle/HOL has been formalized for composing together voting rules from self-contained electoral modules. The composition of modules allows us to translate the verification of a desired property on the module level to the verification of that property for a voting rule implemented by said modules. However, the current composition approach does not deal with modifications of the set of candidates.

In this thesis, we extend the framework by introducing rank offsets as a new composition parameter which enable injection of global information into modules while still allowing modular verification. We show this by proving that the skating system, an algorithm used to rank dancers in ballroom competitions, is monotonous. We evaluate our implementation regarding the compatibility with the framework, generality of our approach, and the scalability of proofs. Our findings are a general pattern for adding new composition mechanisms required by other voting rules.

Literature