Votail: A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections
- Dermot Robert Cochran,
- Joseph Roland Kiniry
Research Output:
Journal Article or Conference Article in Journal
Conference article
Peer-review
Open access
Publication Information
Output type
Research Output:
Journal Article or Conference Article in Journal
Conference article
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 235-252 (17 pages)Journal (Volume, Issue Number)
Karlsruhe Reports in Informatics (Volume 2010, Issue 13)Publication milestones
- Published - 2010
Publication status
Published - 2010
ISSN
2190-4782Abstract
Votail is an open source Java implementation of Irish Proportional Representation by Single Transferable Vote (PR-STV). Its functional requirements, derived from Irish electoral law, are formally specified using the Business Object Notation (BON) and refined to a Java Modeling Language (JML) specification. Formal methods are used to verify and validate the correctness of the software. This is the first public release of a formally verified PR-STV open source system for ballot counting and the most recent of only about half a dozen releases of formally verified e-voting software
Related Event
Title
International Conference on Formal Verification of Object-Oriented Software
Event type
ConferenceDegree of recognition
International eventDate
28/06/2010 - 30/06/2010Location
ParisFrance