Formal Model-based Validation for Tally Systems

Joseph Roland Kiniry, Dermot Cochran, Joseph Roland Kiniry

    Research output: Conference Article in Proceeding or Book/Report chapterBook chapterResearchpeer-review


    Existing commercial and open source e-voting systems have horrifically poor testing frameworks. Most tally systems, for example, are tested by re-running all past elections and seeing if the new system gives the same answer as an older, perhaps erroneous, system did. This amounts to a few dozen system tests and, typically, few-to-no unit tests. These systems are used today in a dozen countries to determine the out- come of national elections. This state-of-affairs cannot continue because it calls into question the legitimacy of elections in major European and North American democracies.

    In this work, the ballot counting process for one of the most complex electoral schemes used in the world, Proportional Representation by Single Transferable Vote (PR-STV), is mechanically formally modeled. The purpose of such a formalization is to generate, using an algorithm of our design, a complete set of non-isomorphic test cases per electoral scheme, once and for all. Using such a system test suite, any digital election technology (proprietary or open source) can be rigorously evaluated for correctness. Doing so will vastly improve the confidence experts have— and can only improve the level of trust citizens have—in these digital elections systems.
    Original languageEnglish
    Title of host publication E-Voting and Identify
    PublisherSpringer VS
    Publication date18 Jul 2013
    ISBN (Print)978-3-642-39184-2
    Publication statusPublished - 18 Jul 2013
    EventThe 4th International Conference on e-Voting and Identity - Guilford, United Kingdom
    Duration: 17 Jul 201319 Jul 2013
    Conference number: 4


    ConferenceThe 4th International Conference on e-Voting and Identity
    Country/TerritoryUnited Kingdom
    Internet address
    SeriesLecture Notes in Computer Science


    • e-voting systems
    • testing frameworks
    • Proportional Representation by Single Transferable Vote (PR-STV)
    • formal modeling
    • test case generation


    Dive into the research topics of 'Formal Model-based Validation for Tally Systems'. Together they form a unique fingerprint.

    Cite this