Skip navigation
Skip navigation

Proving the monotonicity criterion for a plurality vote-counting program as a step towards verified vote-counting

Gore, Rajeev; Meumann, Thomas

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]

CollectionsANU 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 SizeFormat Image
01 Gore and Meumann Proving the monotonicity 2014.pdf188.1 kBAdobe PDFThumbnail


Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator