@inproceedings{98fe4796417948b1a298b6b3da7bdae7,
title = "Modular Formalisation and Verification of STV Algorithms",
abstract = "We introduce a formal, modular framework that captures a large number of different instances of the Single Transferable Vote (STV) counting scheme in a uniform way. The framework requires that each instance defines the precise mechanism of counting and transferring ballots, electing and eliminating candidates. From formal proofs of basic sanity conditions for each mechanism inside the Coq theorem prover, we then synthesise code that implements the given scheme in a provably correct way and produces a universally verifiable certificate of the count. We have applied this to various variations of STV, including several used in Australian parliamentary elections and demonstrated the feasibility of our approach by means of real-world case studies.",
author = "Ghale, {Milad K.} and Rajeev Gor{\'e} and Dirk Pattinson and Mukesh Tiwari",
note = "Publisher Copyright: {\textcopyright} 2018, Springer Nature Switzerland AG.; 3rd International Joint Conference on Electronic Voting, E-Vote-ID 2018 ; Conference date: 02-10-2018 Through 05-10-2018",
year = "2018",
doi = "10.1007/978-3-030-00419-4_4",
language = "English",
isbn = "9783030004187",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "51--66",
editor = "Robert Krimmer and David Duenas-Cid and Melanie Volkamer and Veronique Cortier and Uwe Serdult and Rajeev Gore and Manik Hapsara",
booktitle = "Electronic Voting - Third International Joint Conference, E-Vote-ID 2018, Proceedings",
address = "Germany",
}