Many juristrictions around the world are starting to use computers for casting and counting votes, even at national elections. Two vital but orthogonal questions arise: 1: Are the votes recorded, transmitted and stored correctly and securely? 2: Are the stored votes counted correctly? The first question has received much attention, but the second question has received hardly any because many jurisdictions use a simple "first past the post" method for countig votes. Many jurisdictions in Australia, and especially the Australian Capital Territory, use a single transferable voting scheme which is notoriously hard to count, even with computers.
Our goal is to produce a fully verified vote counting program for single transferable voting, especially the Hare Clark version used in Canberra. Your task will be to familiarise yourself with the problem and contribute to our research. We have done a lot of preliminary work and you would be guided by experts in this field.
You will need a good background in maths and theoretical computer science since all of our work is based on logic. A background in functional programming would also be useful e.g. OCaml or Haskell or ML
Successful completion is likely to lead to a conference paper.
single transferable voting program verification