Vote Counting as Mathematical Proof
- ,
- Dirk Pattinson
- ,
- Australian National University
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-reviewPublication Information
Output type
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 464-475 (11 pages)Publication milestones
- Published - 01/12/2015
Publication status
Published - 01/12/2015
Place of publication
CanberraEdition
2015Volume
LNAI 9457Publisher
Springer, United States, GermanyISBN (Print)
978-3-319-26349-6ISBN (Electronic)
978-3-319-26350-2Publication IDs
- Scopus: 84952643452
Host publication title
Proceedings of 28th Australasian Joint Conference on Artificial IntelligenceHost publication editors
- Bernhard Pfahringer
- Jochen Renz
Abstract
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.
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.
Publication metrics
PlumX
Captures
3
Citations
13