EVA is the main support system used by municipalities and counties in Norway to hold and implement elections. As such, it is critical to society that the system behaves as expected. By using formal methods it can be proven that the system behaves as expected, and that it cannot fail to behave as expected. This work will present EVA and its central aspects, specify the critical properties using the specification language Java Modeling Language, and prove those properties using a formal technique known as automated theorem proving with the assistance of the KeY System. In addition, the Java Modeling Language and the KeY System will be suffciently presented such that the most prominent features and theories can be implemented into other verification efforts, whereas the limitations of the KeY System will be presented and discussed. The sequential, non-distributed nature of the implementation of EVA makes this system a prime target for using deductive verification in an environment were library methods and external frameworks are extensively used. En masse, this work may serve as a guide for others who seek to start a verification project of their own, or to continue and extend the presented work.
| supervisors | Christian Johannsen, Martin Steffen |
| IFI links | abstract, thesis, presentation |