## Vote Counting as Mathematical Proof

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

#### Standard

**Vote Counting as Mathematical Proof.** / Schürmann, Carsten; Pattinson, Dirk.

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

#### Harvard

*Proceedings of 28th Australasian Joint Conference on Artificial Intelligence.*2015 edn, vol. LNAI 9457, Springer, Canberra, pp. 464-475.

#### APA

*Proceedings of 28th Australasian Joint Conference on Artificial Intelligence*(2015 ed., Vol. LNAI 9457, pp. 464-475). Canberra: Springer.

#### Vancouver

#### Author

#### Bibtex

}

#### RIS

TY - GEN

T1 - Vote Counting as Mathematical Proof

AU - Schürmann, Carsten

AU - Pattinson, Dirk

PY - 2015/12/1

Y1 - 2015/12/1

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.

M3 - Article in proceedings

SN - 978-3-319-26349-6

VL - LNAI 9457

SP - 464

EP - 475

BT - Proceedings of 28th Australasian Joint Conference on Artificial Intelligence

A2 - Pfahringer, Bernhard

A2 - Renz, Jochen

PB - Springer

CY - Canberra

ER -

ID: 80595072