@inproceedings{4b013c682ee04f809c7c71a5b8620a2c,
title = "Proving the monotonicity criterion for a plurality vote-counting program as a step towards verified vote-counting",
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.",
author = "Rajeev Gore and Thomas Meumann",
note = "Publisher Copyright: {\textcopyright} 2014 E-Voting.CC.; 6th International Conference on Electronic Voting, EVOTE 2014 ; Conference date: 28-10-2014 Through 31-10-2014",
year = "2015",
month = jan,
day = "1",
doi = "10.1109/EVOTE.2014.7001138",
language = "English",
series = "2014 6th International Conference on Electronic Voting: Verifying the Vote - IEEE Proceedings EVOTE 2014",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
editor = "Robert Krimmer and Melanie Volkamer",
booktitle = "2014 6th International Conference on Electronic Voting",
address = "United States",
}