DiVS: Danish Voting System
DiVS is an implementation that covers (almost) all procedures of the Danish elections to the Folketing from the Election Day until the final result is computed; this includes both the preliminary counting on Election Night and the final careful recounting of the votes starting the day after the Election Day. DiVS covers only the election in Denmark (175 seats), because Greenland (2 seats) and Faroe Islands (2 seats) use different rules. A few aspects have been left out, like party list and substitution list.
The functional requirements translated from the Danish law text are specified using Business Object Notation (BON) and Java Modeling Language (JML). The verification of the correctness is made by formal methods. The tools currently available for checking the soundness of Java implementations version 1.6 are not yet mature. Therefore the correctness has been verified by manual outlining of a proof.