TY - JOUR
TI - Vote Counting as Mathematical Proof
LA - eng
PB - Springer
AU - SchÃ¼rmann, Carsten
AU - Pattinson, Dirk
A2 - Pfahringer, Bernhard, Renz, Jochen
JF - Proceedings of 28th Australasian Joint Conference on Artificial Intelligence
SP - 464
EP - 475
PY - 2015
SN - 9783319263496, 9783319263502
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.
ER -