Proving the monotonicity criterion for a plurality vote-counting program as a step towards verified vote-counting
Download (188.1 kB)
-
Altmetric Citations
Description
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 |
---|---|
Date published: | 2014 |
Type: | Conference paper |
URI: | http://hdl.handle.net/1885/13462 |
Source: | 2014 6th International Conference on Electronic Voting: Verifying the Vote, EVOTE 2014 - IEEE Proceedings |
DOI: | 10.1109/EVOTE.2014.7001138 |
Download
File | Description | Size | Format | Image |
---|---|---|---|---|
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.
Updated: 17 November 2022/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator