Abstract
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.
| Original language | English |
|---|
| Publisher | IT-Universitetet i København |
|---|---|
| Number of pages | 166 |
| ISBN (Print) | 978-87-7949-271-4 |
| Publication status | Published - 2012 |
| Series | ITU-DS |
|---|---|
| Number | 81 |
| ISSN | 1602-3536 |