Computational social choice is a rapidly evolving research trend concerned with the design and analysis of methods for collective decision making. It combines methods from computer science with insights from economic theory. COST Action IC1205 on Computational Social Choice is a European research network that has been set up to provide a common platform for research in this field across Europe and beyond.
Within this project, we focus on the specification and verification of voting rules. A voting rule, as a method to combine individual preferences to an aggregated election result, is part of the fundamental democratic principles. It is thus vital that voting rules are working as intended. Existing voting rules have shown undesired and sometimes surprising properties (e.g., negative voting weights in federal elections in Germany) — for more complicated, newly designed voting rules which become possible due to computer assistance in the vote counting process, these issues are likely to emerge as well.
The goal of this project is to develop formal verification techniques which allow to check properties of voting rules without the huge overhead of user interaction needed in full functional verification. The resulting methodology could then be used in an iterative design and implementation process of new voting rules.
Findings within this project are furthermore applied within FairNet RIC:
The FairNet Research and Innovation Center aims at enabling an internet that offers a variety of value-oriented services among which consumers can choose from easy to manage, transparent, and reliable options.
Values are abstract concepts of the desirable and exist on an individual, economic as well as on a business level.
Internet-based services are value-based and this often results in value conflicts between consumers, providers,
These close interdependencies between informative, social, regulatory and economic aspects constitute a challenge for research and practice.
In the FairNet RIC, researchers from various disciplines – computer science, information systems, psychology, business administration, economics, ethics and law – collaborate interdisciplinary to facilitate the socio-technical design of value-oriented Internet-based services.
|Bernhard Beckert||Prof. Dr.||+49 721 608 44025||beckert∂kit.edu|
|Michael Kirsten||+49 721 608 45648||kirsten∂kit.edu|
|Mattias Ulbrich||Dr.||+49 721 608 44338||ulbrich∂kit.edu|
If you are a KIT student in computer science and interested in writing your thesis within the scope of this project, feel free to contact Michael Kirsten. We also have open positions for student assistants ("HiWi") working on the project.
|Towards automatic argumentation about voting rules||Michael Kirsten and Olivier Cailloux||4ème Conférence Nationale sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018)|
|An Introduction to Voting Rule Verification||Bernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Carsten Schürmann||Trends in Computational Social Choice, Part II: Techniques|
|Formal Fairness Properties in Network Routing Based on a Resource Allocation Model||Almut Demel and Michael Kirsten||9th Workshop on Logical Aspects of Multi-Agent Systems (LAMAS 2017) affiliated with CSL 2017: the 26th EACSL Annual Conference on Computer Science Logic|
|Automatic Margin Computation for Risk-Limiting Audits||Bernhard Beckert, Michael Kirsten, Vladimir Klebanov, and Carsten Schürmann||First International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016)|
|Automated Verification for Functional and Relational Properties of Voting Rules||Bernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber, and Mattias Ulbrich||Sixth International Workshop on Computational Social Choice (COMSOC 2016)|
|Formal Verification of Voting Schemes||Michael Kirsten||ITI Beckert, Karlsruhe Institute of Technology (December 2014)|
|Reasoning About Vote Counting Schemes Using Light-Weight and Heavy-Weight Methods||Bernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Thomas Meumann||8th International Verification Workshop (VERIFY 2014) in connection with IJCAR 2014: International Joint Conference on Automated Reasoning|
|Verifying Voting Schemes||Bernhard Beckert, Rajeev Goré, Carsten Schürmann, Thorsten Bormer, and Jian Wang||Journal of Information Security and Applications (JISA) 19(2)|
|On the Specification and Verification of Voting Schemes||Bernhard Beckert, Rajeev Goré, and Carsten Schürmann||4th International Conference on E-Voting and Identity (Vote-ID 2013)|
|Analysing Vote Counting Algorithms Via Logic - And its Application to the CADE Election System||Bernhard Beckert, Rajeev Goré, and Carsten Schürmann||24th International Conference on Automated Deduction (CADE-24)|