Bounded Verification of Fairness Properties for Seat Apportionment Methods
| Forschungsthema: | Computational Social Choice |
|---|---|
| Typ: | BA |
| Datum: | 2021-01-21 |
| Betreuer: | Michael Kirsten |
| Aushang: |
Abstract
This thesis examines efficient verification techniques for analyzing fairness properties of seat apportionment methods. Seat apportionment methods are algorithms in proportional elections that determine the number of seats for each eligible party. Within this thesis, we investigate a range of optimization techniques based on the formal method known as software bounded model checking. Within an extensive case study, we model and analyze seven apportionment methods and 16 desired fairness properties from the literature as C programs. We implement and evaluate various different back-ends and options of the bounded model checking tool CBMC. Moreover, we evaluate different ways of implementing the investigated apportionment methods and two optimization techniques, in order to reach higher input bounds. The results for the employed optimization techniques and improved implementations show an advantageous performance. Finally, we employ CBMC's functionality to show program traces in order to generate counterexamples for violated fairness properties.
Literature
- "Automated Verification for Functional and Relational Properties of Voting Rules" in Sixth International Workshop on Computational Social Choice (COMSOC 2016)
- "Towards automatic argumentation about voting rules" in 4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018)