Skip navigation
Skip navigation

Verified and Verifiable Computation with STV Algorithms

Ketab Ghale Haji Ali, Milad

Description

Single Transferable Vote (STV) is a family of preferential voting systems, different instances of which are used in binding elections throughout the world. Most countries with an STV system rely on archaic manual vote counting or opaque unreliable computerised methods. Although technology exists to enhance the situation by building significantly more transparent, trustworthy, reliable vote counting tools, in practice these technologies are ignored. We introduce a framework which formalises and...[Show more]

dc.contributor.authorKetab Ghale Haji Ali, Milad
dc.date.accessioned2019-10-15T13:08:46Z
dc.date.available2019-10-15T13:08:46Z
dc.identifier.urihttp://hdl.handle.net/1885/176977
dc.description.abstractSingle Transferable Vote (STV) is a family of preferential voting systems, different instances of which are used in binding elections throughout the world. Most countries with an STV system rely on archaic manual vote counting or opaque unreliable computerised methods. Although technology exists to enhance the situation by building significantly more transparent, trustworthy, reliable vote counting tools, in practice these technologies are ignored. We introduce a framework which formalises and verifies the similarities of STV algorithms as an abstract machine and realises differences of various STV algorithms as instantiations into the machine. The framework provides a uniform and modular process of (a) producing tools that carry out verified computation with an STV algorithm and (b) synthesising means for verifying the computation carried out independently of the computation's source code. It also provides flexibility and ease for adapting and extending it to a variety of STV schemes. We minimise the trusted base in the correctness of the tools synthesised by using the Coq and HOL4 theorem provers and the ecosystem of CakeML as the technical basis. Moreover, we automate almost all proofs that we establish in Coq, HOL4 and CakeML so that new instances of verified and verifying tools for computation with a variety of STV algorithms can be created with no (or minimal) extra verification. Finally, our experimental results with executable code demonstrate the feasibility of deploying the framework for verifying real size elections having an STV counting mechanism.
dc.language.isoen_AU
dc.titleVerified and Verifiable Computation with STV Algorithms
dc.typeThesis (PhD)
local.contributor.supervisorPattinson, Dirk
local.contributor.supervisorcontactu4762643@anu.edu.au
dc.date.issued2019
local.contributor.affiliationCollege Engineering & Computer Science, The Australian National University
local.identifier.proquestYes
local.thesisANUonly.author6163e91a-656a-4ea2-9eb1-38d25ab5776f
local.thesisANUonly.title000000015382_TC_1
local.thesisANUonly.key6d5be6d8-eeba-20e1-15d7-8d177876890b
CollectionsOpen Access Theses

Download

File Description SizeFormat Image
MyThesisFinal.pdfThesis Material2.04 MBAdobe PDFThumbnail


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator