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 JournalConference articleResearchpeer-review

    Abstract

    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

    Original languageEnglish
    JournalKarlsruhe Reports in Informatics
    Volume2010
    Issue number13
    Pages (from-to)235-252
    Number of pages17
    ISSN2190-4782
    Publication statusPublished - 2010
    EventInternational Conference on Formal Verification of Object-Oriented Software - Paris, France
    Duration: 28 Jun 201030 Jun 2010
    http://foveoos2010.cost-ic0701.org/

    Conference

    ConferenceInternational Conference on Formal Verification of Object-Oriented Software
    Country/TerritoryFrance
    CityParis
    Period28/06/201030/06/2010
    Internet address

    Keywords

    • Votail
    • Proportional Representation
    • Single Transferable Vote
    • Formal Verification
    • E-Voting Software

    Fingerprint

    Dive into the research topics of 'Votail: A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections'. Together they form a unique fingerprint.
    • Verifiable Elections

      Kiniry, J. R. (PI) & Cochran, D. (PI)

      01/01/201001/01/2012

      Project: Research

    Cite this