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