Verified Efficient Implementation of Modular Voting Rules Using Stepwise Refinement in Isabelle/HOL

Forschungsthema:Computational Social Choice
Typ: MA
Datum: 2022-09-15
Betreuer: Michael Kirsten


A voting rule is a function that maps the individual voters' preferences among the available alternatives to a set of winning alternatives. For verifying the fairness of such formally specified voting rules, a formal framework has been developed within Isabelle/HOL that is based on formal rules for the construction of voting rules. However, the verified executable code that Isabelle generates for the voting rules is significantly slower than their C implementations.
In this thesis, we use stepwise refinement to generate verified efficient implementations of the voting rules in the framework. The refined code is generated from monadic functions where abstract data structures such as sets and relations are represented by arrays. Moreover, we investigate how the modular structure of the framework's voting rule construction can be used in the refinement proofs.