Dutch Election Software
Nov. 16, 2012 – 4 years, 5 months ago, by erikpoll
Verify the software that computes the seat allocation in Dutch elections.
About 5 kLoc of Java code, see Supplementary Materials.
The Dutch Election law (about six pages of legal prose), see Supplementary Materials.
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).
- Election council page on software (Dutch)
- Dutch election law (English, chapter P is relevant)