Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Automated Verification and Generation of Voting Rules Using Composable Modules

Forschungsthema:Computational Social Choice
Typ: MA
Datum: 2020-06-02
Betreuer: Michael Kirsten
Aushang:

Abstract

Voting rules describe how a collective decision can be derived from a collection of individual decisions. While a voting rule should obviously be fair, it is far from obvious what being fair even means. While an individual notion of fairness might exist, it is insufficient for formal analysis of voting rules. Therefore, voting rules and their properties have been formally defined and examined using methods of mathematics and formal logics, and it was proven that no single voting rule can satisfy all intuitively desirable properties.
In this thesis, we present an automatic approach to the generation of voting rules satisfying certain properties. It is based on a modular framework verified within Isabelle/HOL for constructing voting rules as compositions of simple modules. This allows for proving properties of voting rules in a structured manner from properties of the smaller components. This generation process is implemented and automated such that from a given set of desired properties, an executable voting rule satisfying those is automatically generated, if possible. Moreover, we automatically generate a machine-verified proof that the voting rule does indeed satisfy the required properties. The pipeline can also be used to generate proofs for properties of user-specified voting rules. As a theoretical foundation, we formally define the voting rule generation as a decision problem and prove its general decidability. From this, we obtain well-founded claims decidability results of whether a voting rule satisfying some properties can be defined within the framework or not. Finally, we provide flexible C code snippets for selected modules such that a generated voting rule can be analysed for further properties using the verification technique of software bounded model checking, so that either (for a violated property) we can generate understandable counterexamples, or show that no such counterexample exists up to a specified bound on the number of voters and candidates.

Literature