Applying Software Bounded Model Checking to the Australian Voting Method
| Forschungsthema: | Computational Social Choice |
|---|---|
| Typ: | BA |
| Datum: | 2020-01-01 |
| Betreuer: | Michael Kirsten |
| Aushang: |
Abstract
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.
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)