COST Action IC1205 – Computational Social Choice

Project Description

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.

COST Action

Findings within this project are furthermore applied within FairNet RIC:

Cooperation FairNet RIC - FairNet Research and Innovation Center

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, and governance-stakeholders.
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.

FairNet RIC



Name Title Phone Email
Bernhard Beckert Prof. Dr. +49 721 608-44025 beckert84933776Xfd4∂
Michael Kirsten +49 721 608-45648 kirsten2009682555Xfd4∂


Name Title Phone Email
Mattias Ulbrich Dr. +49 721 608-44338 ulbrich11451541Xfd4∂


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.


Title Author(s) Source
Verified Construction of Fair Voting RulesKarsten Diekhoff, Michael Kirsten, and Jonas Krämer29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019), Revised Selected Papers
Title Author(s) Source
Formal Property-Oriented Design of Voting Rules Using Composable ModulesKarsten Diekhoff, Michael Kirsten, and Jonas Krämer6th International Conference on Algorithmic Decision Theory (ADT 2019), Part Short Papers
GI Elections with POLYAS: a Road to End-to-End Verifiable ElectionsBernhard Beckert, Achim Brelle, Rüdiger Grimm, Nicolas Huber, Michael Kirsten, Ralf Küsters, Jörn Müller‑Quade, Maximilian Noppel, Kai Reinhard, Jonas Schwab, Rebecca Schwerdt, Tomasz Truderung, Melanie Volkamer, and Cornelia WinterFourth International Joint Conference on Electronic Voting (E-Vote-ID 2019)
Title Author(s) Source
Towards automatic argumentation about voting rulesMichael Kirsten and Olivier Cailloux4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018)
Title Author(s) Source
An Introduction to Voting Rule VerificationBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Carsten SchürmannTrends in Computational Social Choice, Part II: Techniques
Formal Fairness Properties in Network Routing Based on a Resource Allocation ModelAlmut Demel and Michael Kirsten9th 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 AuditsBernhard Beckert, Michael Kirsten, Vladimir Klebanov, and Carsten SchürmannFirst International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016)
Title Author(s) Source
Automated Verification for Functional and Relational Properties of Voting RulesBernhard Beckert, Thorsten Bormer, Michael Kirsten, Till Neuber, and Mattias UlbrichSixth International Workshop on Computational Social Choice (COMSOC 2016)
Title Author(s) Source
Formal Verification of Voting SchemesMichael KirstenITI Beckert, Karlsruhe Institute of Technology (December 2014)
Reasoning About Vote Counting Schemes Using Light-Weight and Heavy-Weight MethodsBernhard Beckert, Thorsten Bormer, Rajeev Goré, Michael Kirsten, and Thomas Meumann8th International Verification Workshop (VERIFY 2014) in connection with IJCAR 2014: International Joint Conference on Automated Reasoning
Verifying Voting SchemesBernhard Beckert, Rajeev Goré, Carsten Schürmann, Thorsten Bormer, and Jian WangJournal of Information Security and Applications (JISA) 19(2)
Title Author(s) Source
On the Specification and Verification of Voting SchemesBernhard Beckert, Rajeev Goré, and Carsten Schürmann4th International Conference on E-Voting and Identity (Vote-ID 2013)
Analysing Vote Counting Algorithms Via Logic - And its Application to the CADE Election SystemBernhard Beckert, Rajeev Goré, and Carsten Schürmann24th International Conference on Automated Deduction (CADE-24)