Conference
Proving the monotonicity criterion for a plurality vote-counting program as a step towards verified vote-counting
| العنوان: | Proving the monotonicity criterion for a plurality vote-counting program as a step towards verified vote-counting |
|---|---|
| المؤلفون: | Gore, Rajeev, Meumann, Thomas |
| المصدر: | 2014 6th International Conference on Electronic Voting: Verifying the Vote, EVOTE 2014 - IEEE Proceedings |
| بيانات النشر: | Institute of Electrical and Electronics Engineers Inc. |
| سنة النشر: | 2015 |
| المجموعة: | Australian National University: ANU Digital Collections |
| مصطلحات موضوعية: | Encoding (symbols), Formal logic, Verification, Complex properties, Higher order logic, Interactive theorem prover, Monotonicity, Monotonicity property, Plurality voting, Theorem provers, Verification tools, Theorem proving |
| جغرافية الموضوع: | Lochau, Austria |
| الوصف: | 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. |
| نوع الوثيقة: | conference object |
| وصف الملف: | 7 pages |
| اللغة: | unknown |
| ردمك: | 978-3-200-03697-0 3-200-03697-4 |
| Relation: | 6th International Conference on Electronic Voting: Verifying the Vote (EVOTE) 2014; http://hdl.handle.net/1885/13462; https://openresearch-repository.anu.edu.au/bitstream/1885/13462/5/01+Gore+and+Meumann+Proving+the+monotonicity+2014.pdf.jpg |
| DOI: | 10.1109/EVOTE.2014.7001138 |
| الاتاحة: | http://hdl.handle.net/1885/13462 https://doi.org/10.1109/EVOTE.2014.7001138 https://openresearch-repository.anu.edu.au/bitstream/1885/13462/5/01+Gore+and+Meumann+Proving+the+monotonicity+2014.pdf.jpg |
| Rights: | http://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). |
| رقم الانضمام: | edsbas.DFCD5493 |
| قاعدة البيانات: | BASE |
| ردمك: | 9783200036970 3200036974 |
|---|---|
| DOI: | 10.1109/EVOTE.2014.7001138 |