TY - GEN
T1 - Vote counting as mathematical proof
AU - Pattinson, Dirk
AU - Schürmann, Carsten
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2015.
PY - 2015
Y1 - 2015
N2 - Trust in the correctness of an election outcome requires proof of the correctness of vote counting. By formalising particular voting protocols as rules, correctness of vote counting amounts to verifying that all rules have been applied correctly. A proof of the outcome of any particular election then consists of a sequence (or tree) of rule applications and provides an independently checkable certificate of the validity of the result. This reduces the need to trust, or otherwise verify, the correctness of the vote counting software once the certificate has been validated. Using a rule-based formalisation of voting protocols inside a theorem prover, we synthesise vote counting programs that are not only provably correct, but also produce independently verifiable certificates. These programs are generated from a (formal) proof that every initial set of ballots allows to decide the election winner according to a set of given rules.
AB - Trust in the correctness of an election outcome requires proof of the correctness of vote counting. By formalising particular voting protocols as rules, correctness of vote counting amounts to verifying that all rules have been applied correctly. A proof of the outcome of any particular election then consists of a sequence (or tree) of rule applications and provides an independently checkable certificate of the validity of the result. This reduces the need to trust, or otherwise verify, the correctness of the vote counting software once the certificate has been validated. Using a rule-based formalisation of voting protocols inside a theorem prover, we synthesise vote counting programs that are not only provably correct, but also produce independently verifiable certificates. These programs are generated from a (formal) proof that every initial set of ballots allows to decide the election winner according to a set of given rules.
UR - http://www.scopus.com/inward/record.url?scp=84952643452&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-26350-2_41
DO - 10.1007/978-3-319-26350-2_41
M3 - Conference contribution
AN - SCOPUS:84952643452
SN - 9783319263496
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 464
EP - 475
BT - AI 2015
A2 - Renz, Jochen
A2 - Pfahringer, Bernhard
PB - Springer Verlag
T2 - 28th Australasian Joint Conference on Artificial Intelligence, AI 2015
Y2 - 30 November 2015 through 4 December 2015
ER -