Applying Bounded Verification to the German Seat Distribution Procedure
| Forschungsthema: | Social Choice |
|---|---|
| Typ: | BA |
| Datum: | 2017-07-12 |
| Betreuer: | Michael Kirsten |
| Aushang: |
Beschreibung
Im Jahr 2008 fand das deutsche Verfassungsgericht heraus, dass das Wahlverfahren
zur Bestimmung des deutschen Bundestags verfassungswidrig ist. Der Grund waren
negative Stimmgewichte, die dazu führten, dass manche Stimmen mehr Gewicht hatten
als andere. Daraufhin wurde schließlich 2013 das Wahlverfahren geändert. Am
Lehrstuhl für Anwendungsorientierte Formale Verifikation entwickeln wir Methoden, um
Implementierungen von Wahlverfahren auf solche und ähnliche Eigenschaften hin zu
analysieren.
Insbesondere mithilfe der Technik Bounded Model Checking lässt sich dies gut
automatisieren. Im Rahmen einer Abschlussarbeit wäre es hier interessant, diese
Technik auch auf das deutsche Wahlverfahren anzuwenden und zum Einen zu prüfen
inwieweit das neue Verfahren das Problem (die zu prüfende Eigenschaft wäre
"Monotonie") nun gelöst hat, aber auch inwieweit andere Eigenschaften erfüllt
werden, wie bspw. Anonymität, d.h., dass es für das Wahlergebnis unerheblich ist,
in welcher Reihenfolge die Stimmen abgegeben werden.
Voraussetzungen
- Grundkenntnisse in und Interesse an formalen Methoden, wie sie z. B. in der Vorlesung Formale Methoden vermittelt werden
- Gründliche Arbeitsweise sowie ein gutes Abstraktionsvermögen
Kontakt
Interesse? Weitergehende Fragen? Dann melden Sie sich unverbindlich bei Michael Kirsten (Raum 228, Geb. 50.34).
Literatur
- "Automated Verification for Functional and Relational Properties of Voting Rules" in Sixth International Workshop on Computational Social Choice (COMSOC 2016)