Compositional Verification of Social Choice Properties for Single Transferable Vote Using an Interactive Theorem Prover
|Forschungsthema:||Computational Social Choice|
Decisions need to be made in many situations, both for high-stakes occasions
such as presidential or parliamentary elections, for boards of trustees, but
also in low-stakes every life such as deciding which restaurant to go to as a
group of friends.
A famous method in the case of elections is the Single Transferable Vote (STV)
which allows to rank candidates by preference.
STV then iteratively eliminates options with the least amount of top
preferences by transfering their votes to the next preferred option until a
clear winner is found, however throughout the world different variants of STV
are in use.
Within this thesis, we want to prove interesting fairness properties such as the clone-proofness property for selected variants of STV. As STV is rather complex and has many variants, we want to decompose STV into smaller manageable parts using a modular composition framework verified within the interactive theorem prover Isabelle/HOL. By this, we want to flexibly parameterize and compose general variants of STV together with correct-by-construction proofs that the properties of interest are satisfied.
- "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)