Proving the monotonicity criterion for a plurality vote-counting program as a step towards verified vote-counting
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...[Show more]
|Collections||ANU Research Publications|
|Source:||2014 6th International Conference on Electronic Voting: Verifying the Vote, EVOTE 2014 - IEEE Proceedings|
|01 Gore and Meumann Proving the monotonicity 2014.pdf||188.1 kB||Adobe PDF|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.