Dutch Election Software

Nov. 16, 2012 – 4 years, 4 months ago, by erikpoll

Short Description

Verify the software that computes the seat allocation in Dutch elections.

Code

About 5 kLoc of Java code, see Supplementary Materials.

Specification

The Dutch Election law (about six pages of legal prose), see Supplementary Materials.

Long Description

After recent controversy around voting computers, the Dutch goverment has also reconsidered the software that computes the seat allocation in an election. An invitation for offers was put out for a new implementation of this election software. It should use open standards and be open source. The winning bid was a Java implementation and has already been used in the 2009 election for the Dutch members of European Parliament.

The following requirement in the offer was not met by the new implementation:

With the help of formal methods, it has been mathematically shown that the computations do what is required by law and rules.

The developers of the software did produce a hand-written mathematical specification that relates to both the Dutch election law and their Java implementation.

This formal-methods requirement appears out of reach for the state-of-the-art (2009) in Java program verification. It does make for a interesting challenge:

  • Correctness is essential.
  • It is a real-world program.
  • The size of the Java program is modest (about 5 kLoc).

Supplementary Materials

We have a local copy of the software and the formal specification.

Submitted by

Ronny Wichers Schreur, edited by verifythis@cost-ic0701.org