@inproceedings{c99c9ed05e304ab9ab8152875fa79024,
title = "Verified Certificate Checking for Counting Votes",
abstract = "We introduce a new framework for verifying electronic vote counting results that are based on the Single Transferable Vote scheme (STV). Our approach frames electronic vote counting as certified computation where each execution of the counting algorithm is accompanied by a certificate that witnesses the correctness of the output. These certificates are then checked for correctness independently of how they are produced. We advocate verification of the verifier rather than the software used to produce the result. We use the theorem prover HOL4 to formalise the STV vote counting scheme, and obtain a fully verified certificate checker. By connecting HOL4 to the verified CakeML compiler, we then extract an executable that is guaranteed to behave correctly with respect to the formal specification of the protocol down to machine level. We demonstrate that our verifier can check certificates of real-size elections efficiently. Our encoding is modular, so repeating the same process for another different STV scheme would require a minimal amount of additional work.",
author = "Ghale, {Milad K.} and Dirk Pattinson and Ramana Kumar and Michael Norrish",
note = "Publisher Copyright: {\textcopyright} 2018, Springer Nature Switzerland AG.; 10th International Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2018 ; Conference date: 18-07-2018 Through 19-07-2018",
year = "2018",
doi = "10.1007/978-3-030-03592-1_5",
language = "English",
isbn = "9783030035914",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "69--87",
editor = "Ruzica Piskac and Philipp R{\"u}mmer",
booktitle = "Verified Software. Theories, Tools, and Experiments - 10th International Conference, VSTTE 2018, Revised Selected Papers",
address = "Germany",
}