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

Verified Construction of the Instant-Runoff Voting Rule

Forschungsthema:Computational Social Choice
Typ: BA
Datum: 2023-07-27
Betreuer: Michael Kirsten
Aushang:

Abstract

The investigation of voting rules by employing computational and formal methods and verifying associated criteria can provide insights into the design and application of how we conduct voting procedures, which is potentially critical for society at large.

In this thesis, we extend a framework for modeling and formally verifying voting rules within the theorem prover Isabelle/HOL by implementing the instant-runoff voting (IRV) rule and the property independence of clones (IC). IRV requires voters to rank candidates in order of preference and ballots are initially counted for each voter’s top choice. If an alternative garners more than half of these votes, they emerge victorious. If not, the alternative with the fewest top votes is eliminated, and their votes are reassigned to the remaining alternatives based on the ballots’ second choices. This process is repeated until an alternative secures a majority. Finally, the IC property requires that if one or more similar alternatives to anexiasting one are added to the election, it should not impact the existing alternative’s chances of winning. IC safeguards a good alternative from losing merely because the vote is split between the alternative aspiring to win and its ’clones.’

We present the implementation and modeling of IRV within the framework, together with new basic functionalities for eliminating alternatives in a voting procedure. Finally, we discuss the challenges encountered during the translation from literature to a formal, verifiable language and describe our approach for formally verifying IRV for the IC property.

Literature