Automatic Margin Computation for Risk-Limiting Audits
Bernhard Beckert, Michael Kirsten, Vladimir Klebanov, and Carsten Schürmann
A risk-limiting audit is a statistical method to create confidence in the
correctness of an election result by checking samples of paper ballots. In
order to perform an audit, one usually needs to know what the election margin
is, i.e., the number of votes that would need to be changed in order to change
the election outcome. In this paper, we present a fully automatic method for
computing election margins. It is based on the program analysis technique of
bounded model checking to analyse the implementation of the election function.
The method can be applied to arbitrary election functions without
understanding the actual computation of the election result or without even
intuitively knowing how the election function works. We have implemented our
method based on the model checker CBMC; and we present a case study
demonstrating that it can be applied to real-world elections.