Formal Specification and Analysis of Danish and Irish Ballot Counting Algorithms
- Dermot Cochran
Research Output:
Theses
PhD thesis
Open access
Publication Information
Output type
Research Output:
Theses
PhD thesis
Original language
EnglishQualification
PhDPublication milestones
- Published - 2012
Publication status
Published - 2012
Supervisors/Advisors
- Joseph Roland Kiniry (Principal Supervisor)
Award date
10/09/2012Publisher
IT-Universitetet i København, DenmarkBook series
- Book series name: ITU-DS
Series number: 81
ISSN: 1602-3536
ISBN (Print)
978-87-7949-271-4Abstract
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.
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.
Access to documents
Final published version, 1022.1 KB