Applied Formal Methods for Elections

Information technology is changing the way elections are organized. Technology renders the electoral process more efficient, but things could also go wrong: Voting software is complex, it consists of over thousands of lines of code, which makes it error-prone. Technical problems may cause delays at polling stations, or even delay the announcement of the final result. This thesis describes a set of methods to be used, for example, by system developers, administrators, or decision makers to examine election technologies, social choice algorithms and voter experience.
Technology: Verifiability refers to voting software producing evidence so that can be retroactively analyzed, in case that something went wrong. There are two possible ways to analyze implementations for verifiability, first statically, i.e. before the technology is deployed, which gives the developers the opportunity to fix issues during development time, or second dynamically, i.e. monitoring while an implementation is used during an election, or after the election is over, for forensic analysis.
This thesis contains two chapters on this subject: the chapter Analyzing Implementations of Election Technologies describes a technique for checking verifiability properties directly on the source code of e-voting systems using modern code scanning tools. Verifiability properties are expressed in linear temporal logic, then translated into Büchi automata and checked using off the shelf static analyzers. In the chapter Epistemic Policies for Voting Systems, we turn our attention to the logs generated by e-voting systems for policy compliance checking. The novel contribution is that we use epistemic linear time logic to express properties about distributed e-voting systems that then be checked by model-checkers.
Algorithms: The advances in technology open the possibility that the very algorithms we use in elections are going to evolve. Besides first-past-the-post, there are many variants of D'Hondt, Sainte-Laguë and single transferable vote (STV), and these algorithms continue to be adjusted, evolved, and refined.
The chapter Verifying Voting Schemes focuses on the use of formal methods to ensure that these algorithms have the intended meaning and conform to the desired democratic principles. As a case study, we define two semantic criteria for STV schemes, formulated in first-order logic over the theories of arrays and integers, and show how bounded model-checking and satisfiability modulo theories (SMT) solvers can be used to check these criteria.
Voter Experience: Technology profoundly affects the voter experience. These effects need to be measured and the data should be used to make decisions regarding the implementation of the electoral process.
The chapter Measuring Voter Lines describes an automated data collection method for measuring voters' waiting time, and discusses statistical models designed to provide an understanding of the voter behavior in polling stations.