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]

dc.contributor.authorGore, Rajeev
dc.contributor.authorMeumann, Thomas
dc.coverage.spatialLochau, Austria
dc.date.accessioned2015-05-13T02:55:10Z
dc.date.available2015-05-13T02:55:10Z
dc.date.created29-31 October 2014
dc.identifier.isbn978-3-2000-3697-0
dc.identifier.urihttp://hdl.handle.net/1885/13462
dc.description.abstractWe 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.
dc.format7 pages
dc.publisherInstitute of Electrical and Electronics Engineers Inc.
dc.relation.ispartofseries6th International Conference on Electronic Voting: Verifying the Vote (EVOTE) 2014
dc.rightshttp://www.ieee.org/publications_standards/publications/rights/announcement_author_posting_updated.pdf The policy reaffirms the principle that authors are free to post the accepted version of their article on their personal web sites or those of their employers. Posting of the final, published PDF continues to be prohibited, except for open access articles, whose authors may freely post the final version. (Publisher author posting website 4/9/2017) http://www.ieee.org/publications_standards/publications/rights/rights_policies.html © 2014 International Conference on Electronic Voting EVOTE2014, E-Voting.CC GmbH. © Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works (Publisher journal website 4/9/2017).
dc.source2014 6th International Conference on Electronic Voting: Verifying the Vote, EVOTE 2014 - IEEE Proceedings
dc.subjectEncoding (symbols)
dc.subjectFormal logic
dc.subjectVerification
dc.subjectComplex properties
dc.subjectHigher order logic
dc.subjectInteractive theorem prover
dc.subjectMonotonicity
dc.subjectMonotonicity property
dc.subjectPlurality voting
dc.subjectTheorem provers
dc.subjectVerification tools
dc.subjectTheorem proving
dc.titleProving the monotonicity criterion for a plurality vote-counting program as a step towards verified vote-counting
dc.typeConference paper
local.description.notes6th International Conference on Electronic Voting, EVOTE 2014; Lochau / Bregenz; Austria; 28 October 2014 through 31 October 2014.
local.description.refereedYes
dc.date.issued2014
local.identifier.absfor080203 - Computational Logic and Formal Languages
local.identifier.ariespublicationu4334215xPUB1409
local.publisher.urlhttps://www.ieee.org/
local.type.statusAccepted Version
local.contributor.affiliationGore, Rajeev, Research School of Computer Science, College of Engineering and Computer Science, The Australian National University
local.contributor.affiliationMeumann, Thomas, Research School of Computer Science, College of Engineering and Computer Science, The Australian National University
local.bibliographicCitation.startpage1
local.bibliographicCitation.lastpage7
local.identifier.doi10.1109/EVOTE.2014.7001138
local.identifier.absseo970108 - Expanding Knowledge in the Information and Computing Sciences
dc.date.updated2015-12-10T10:46:18Z
local.identifier.scopusID2-s2.0-84922574928
CollectionsANU Research Publications

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