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 schemes (a.k.a. voting rules). A voting scheme, 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 schemes are working as intended. Existing voting schemes have shown undesired and sometimes surprising properties (e.g., negative voting weights in federal elections in Germany) — for more complicated, newly designed voting schemes 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 schemes 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 schemes.

COST Action



Name Title Phone Email
Bernhard Beckert Prof. Dr. +49 721 608 44025 beckert1632767581Xfd4∂
Michael Kirsten +49 721 608 45648 kirsten1209932808Xfd4∂


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


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
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 2015) 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)