In his recently finished Master’s thesis, Henrik Torland Klev verified (parts of) EVA, the main support system for elections in municipalities and counties in Norway, using the KeY prover.
The EVA system records the basic data needed to conduct elections in Norway, including the parties’ list proposals and the electoral figure. Election results are reported to EVA by municipalities and constituencies. Giving the importance of the system for Norwegian elections, increasing the trust in it by means of formal verification is an endeavor whose importance cannot be overestimated. The primary verification target in the scope of this thesis is a central algorithm implemented in the system, Sainte-Laguë’s modified method.
Specifying EVA components in JML required writing non-trivial contracts and auxiliary specifications, in particular complicated loop invariants. Occasionally, the EVA implementation had to be adapted to a version more suitable for formal verification with KeY1.
As a result of the thesis, “most central methods” of EVA were proved to conform to their specifications. Some methods methods could not be proved within this case study due to their complexity. In addition, Klev reports some problems he had with KeY.
The KeY team very much appreciates the work of Henrik Torland Klev and is grateful for the feedback. We encourage all users of KeY, both those who use the platform as a library and those using it as a verification tool in case studies, to reach out to us in case of problems like those mentioned above; please use our support channels to that end. Furthermore, we are always happy to be contacted and informed about new projects realized using KeY.
1) This is not always the case, also for real-world case studies: For the verification of TimSort and Dual Pivot QuickSort, the original implementation was verified.
