Wartung und Weiterentwicklung von BEAST zur Automatischen Wahlverifikation durch SBMC

Typ:	HiWi
Datum:	2020-02-06
Betreuer:	Michael Kirsten
Aushang:	PDF

Hintergrund

Ein Wahlverfahren (engl. voting rule) ist ein Algorithmus, der aus einer Menge an Einzelentscheidungen ein kollektives Wahlergebnis berechnet. Von solchen Wahlverfahren existieren unzählige verschiedene Arten sowohl im akademischen Bereich als auch bei echten Wahlen. Spätestens seit dem von Kenneth J. Arrow im Jahr 1950 beschriebenen Allgemeinen Unmöglichkeitstheorem ist allerdings klar, dass es nicht möglich ist, aus den Wünschen einer Gesellschaft ein Ergebnis abzuleiten, ohne zumindest gewisse gewünschte Grundsätze aufzugeben.

BEAST

BEAST ist eine am Lehrstuhl entwickelte Software zur automatischen und nutzerfreundlichen Verifikation von Wahlverfahren auf formale Fairnesseigenschaften (sog. social choice Eigenschaften). Dabei werden Wahlverfahren, Eigenschaften und gewünschte Schranken durch Programmtransformation an das Back-End CBMC (Werkzeug zur automatischen Verifikation mit Software Bounded Model Checking) weitergegeben und in eine logische Formel transformiert, die anschließend mithilfe eines SAT/SMT-Solvers gelöst wird. Anschließend wird der Nutzerin entweder eine Erfolgsnachricht (wenn die Eigenschaft gilt) oder ein Gegenbeispiel, in dem die Eigenschaft verletzt wird, präsentiert.

Ihre Aufgabe

Ihre Aufgabe besteht darin, BEAST weiterzuentwickeln und zu warten. Weiterhin soll dessen Skalierbarkeit durch den Einbau relationaler Verifikationstechniken verbessert, die Ausdrucksmöglichkeiten der Spezifikationssprache erweitert, sowie die Darstellung von Gegenbeispielen weiterentwickelt werden. Die Vergütung erfolgt nach den üblichen Sätzen für studentische Hilfskräfte.

Voraussetzungen

• Interesse und Kenntnisse in formalen Sprachen und formalen Methoden.
• Programmierkenntnisse und -erfahrung in Java.
• Gute Abstraktionsfähigkeit und strukturierte Arbeitsweise.
• Motivation für die Analyse abstrakter Algorithmen.

Literatur

1. B. Beckert, T. Bormer, M. Kirsten, T. Neuber, und M. Ulbrich. Automated Verification for Functional and Relational Properties of Voting Rules. COMSOC 2016).
2. M. Kirsten und O. Cailloux. Towards automatic argumentation about voting rules. APIA 2018.
3. E. Clarke, D. Kroening, und F. Lerda. A Tool for Checking ANSI-C Programs. TACAS 2004 (Webseite).

Kontakt

Bei Interesse kontaktieren Sie bitte Michael Kirsten für ein unverbindliches Informationsgespräch.