Formal Specification and Analysis of Danish and Irish Ballot Counting Algorithms

Dermot Cochran

    Research output: Book / Anthology / Report / Ph.D. thesisPh.D. thesis


    There are many valid arguments both for and against the use of electronic voting in real world elections.

    My thesis is that a verification-centric software implementation of a particular algorithm for counting of ballots can be proven correct or shown to be incorrect by an appropriate combination of formal specification, static analysis and testing. Hand counting of paper ballots might no longer be necessary, if we can assume that the digital ballots are valid, not tampered with and a true representation of the paper ballots etc.

    As a case study, the Danish and Irish voting schemes are analyzed in this dissertation, including a discussion of how to generate test cases for the Irish voting scheme.
    Original languageEnglish
    PublisherIT-Universitetet i København
    Number of pages166
    ISBN (Print)978-87-7949-271-4
    Publication statusPublished - 2012


    Dive into the research topics of 'Formal Specification and Analysis of Danish and Irish Ballot Counting Algorithms'. Together they form a unique fingerprint.

    Cite this