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

Formalization and Verification of Proportional Representation Voting Systems using Isabelle/HOL: A Study of D’Hondt and Sainte-Laguë Methods

Forschungsthema:Computational Social Choice
Typ: MA
Datum: 2024-05-18
Betreuer: Michael Kirsten
Aushang:

Abstract

This master's thesis deepens and broadens our understanding of collective decision-making in the face of diverse and conflicting individual preferences. Leveraging the advanced capabilities of Isabelle/HOL, a platform for formal mathematical reasoning, this project investigates the D’Hondt and Sainte-Laguë voting systems on fairness criteria that are essential for fostering democratic governance. Voting systems assume various forms, including plurality, ranked preference, and proportional representation systems, each guided by distinct rules that collectively shape the integrity of the decision-making process.

Using Isabelle/HOL, this study constructs rigorous mathematical models that ensure precision and consistency in the analysis of the D’Hondt and Sainte-Laguë voting systems and involves the formalization and verification of anonymity and monotonicity. Anonymity ensures that individual preferences remain confidential, safeguarding the democratic process against undue influence, while monotonicity scrutinizes the consistency of outcomes when preferences are altered. As such, the study presents practical implications for the design and implementation of voting systems.

Literature