Applying Software Bounded Model Checking to the Australian Voting Method

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


The goal of this thesis is to formally verify the algorithm used to perform the election of the House of Representatives of the Commonwealth of Australia. The tool used to carry out this examination is CBMC, a bounded model checker for C-code. Bounded model checking is a variant of model checking which performs verification up to a given bound. Voting algorithms are bounded by their input parameters - that is, the number of voters and candidates. In the case of voting algorithms, bounded model checking hence provides a sufficient way of asserting certain characteristics for smaller instances of the input parameters.
The Australian voting algorithm is inspected with CBMC for certain properties which are established in social choice theory which deals with the mathematical analysis of elections. First, the voting algorithm and the properties are implemented. Second, the algorithm is checked for the properties up to the limit of feasible parameters. Afterwards, run-time optimizations are presented and tested. Finally, the results of the verification are evaluated and discussed.