Bounded Verification of Fairness Properties for Seat Apportionment Methods

Forschungsthema:Computational Social Choice
Typ: BA
Datum: 2021-01-21
Betreuer: Michael Kirsten


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.