Veryfing the Sainte Lagues algorithm for election management in Norway
This topic involves understanding and modelling the election management algorithm Sainte Lagues, which is developed/maintained by UiO people (students and researchers led by Bernt Aardal). Moreover, the topic involves working with verification techniques and tools, both for algorithms but also for code. The programming language is TypeScript.
This topic will model the Sainte Lagues algorithm which is the official system for election management in Norway, as specified in the Lovdata [§11-3, §11-6, §59]. The ultimate goal of the modelling is to verify the properties expected of this algorithm.
However, it is a known issue in verification that errors can be inserted when implementing the algorithm. Therefore, it is also important to verify the implemented code as being deployed and used. We have access to the code, which is not common since usually implementations are kept proprietary by companies. In our case the algorithm is implemented in an open fashion by people that we can interact with.
For verifying code there are different techniques and tools than for verifying algorithms.
The student would learn model checking techniques and tools applicable to general algorithms as well as to code, specifically focusing on the programming language TypeScript that was used to implement the algorithm.
Spin is one tool that is essentially working with C-like programs.
The course INF5140 teaches model checking using Spin.
Ask for discussions with one of the supervisors, for more information or variations of the project. See also general concerns.