Student research opportunities
Verifiably Correct Vote Counting
Project Code: CECS_1137
This project is available at the following levels:
CS single semester, Honours, Summer Scholar, Masters, PhD
Keywords:
Electronic Voting, Interactive Theorem Proving, Verifiability
Supervisor:
Dr Dirk PattinsonOutline:
To gain trust in election outcomes, we formalise voting protocols, such as Hare-Clark used in Australia, as a set of (counting) rules. Counting the votes correctly then amounts to demonstrating that these rules have been applied correctly. The sequence of rule applications then serves as an independently verifiable certificate that attests to the correctness of the count.
Goals of this project
The primary goal of this project is to test the applicability of this idea to real-world voting protocols. There are many avenues:
- the formalisation of different voting protocols as counting rules
- to generate a provably correct vote counting program with the help of an interactive theorem prover
- to formally establish meta-properties of voting protocols on the basis of a rule-based formulation
Requirements/Prerequisites
Background in Functional Programming and/or Formal Methods and/or Interactive Theorem Proving and/or Electronic Voting.
Student Gain
Hands-on experience in the area of software correctness and interactive theorem proving.
Background Literature
A case study that describes the generation of the vote counting programs is avaliable at
http://users.cecs.anu.edu.au/~dpattinson/Software
which contains instructions on how to build and run the case studies.
