Automatic Margin Computation for Risk-Limiting Audits

Bernhard Beckert, Michael Kirsten, Vladimir Klebanov, Carsten Schürmann

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


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.
Original languageEnglish
Title of host publicationFirst International Joint Conference, E-Vote-ID 2016, Bregenz, Austria, October 18-21, 2016, Proceedings
Publication date2017
ISBN (Print)978-3-319-52239-5
ISBN (Electronic)978-3-319-52240-1
Publication statusPublished - 2017
SeriesLecture Notes in Computer Science


Dive into the research topics of 'Automatic Margin Computation for Risk-Limiting Audits'. Together they form a unique fingerprint.

Cite this