Proving the monotonicity criterion for a plurality vote-counting program as a step towards verified vote-counting
Date
2014
Authors
Gore, Rajeev
Meumann, Thomas
Journal Title
Journal ISSN
Volume Title
Publisher
Institute of Electrical and Electronics Engineers Inc.
Abstract
We show how modern interactive verification tools
can be used to prove complex properties of vote-counting software.
Specifically, we give an ML implementation of a votecounting
program for plurality voting; we give an encoding of
this program into the higher-order logic of the HOL4 theorem
prover; we give an encoding of the monotonicity property in the
same higher-order logic; we then show how we proved that the
encoding of the program satisfies the encoding of the monotonicity
property using the interactive theorem prover HOL4. As an aside,
we also show how to prove the correctness of the vote-counting
program. We then discuss the robustness of our approach.
Description
Keywords
Encoding (symbols), Formal logic, Verification, Complex properties, Higher order logic, Interactive theorem prover, Monotonicity, Monotonicity property, Plurality voting, Theorem provers, Verification tools, Theorem proving
Citation
Collections
Source
2014 6th International Conference on Electronic Voting: Verifying the Vote, EVOTE 2014 - IEEE Proceedings
Type
Conference paper