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 |
| Aushang: |
Abstract
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.
Literature
- "Automated Verification for Functional and Relational Properties of Voting Rules" in Sixth International Workshop on Computational Social Choice (COMSOC 2016)
- "Verified Construction of Fair Voting Rules" in 29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019)