Applying Relational Techniques for the Deductive Verification of Voting Systems

Forschungsthema:	KeY, Social Choice
Typ:	BA
Datum:	2015-10-19
Betreuer:	Thorsten Bormer Mattias Ulbrich Michael Kirsten
Aushang:

Abstract

In this bachelor thesis we apply relational verification techniques to prove relational properties of voting systems in various case studies. The goal of this work is to show that this is a feasible approach, which holds advantages over using purely functional verification methods.
The voting systems examined in this work are Majority Voting, Approval Voting, Range Voting and Borda Count. We cover the relational properties Anonymity, Neutrality, Homogeneity, Participation and Monotonicity.
We use an existing approach from Barthe et al. to reduce a relational verification problem to a verification task that can be tackled with the deductive verification tool KeY. In case studies, we prove that the relational properties hold for the mentioned voting systems by presenting a corresponding specification that we verified using the KeY tool. We also conduct a case study in which we automatically generate a counterexample that shows that a property does not hold for a voting system, and a case study where we directly compare a functional with a relational specification of a property.
We show that formulating a relational specification can be done intuitively and is not more complex than formulating a comparable functional specification. We also show that using relational methods can ease the verification process. In the course of this work we discuss several techniques that help to cope with relational verification tasks, notably splitting up a method and rolling out loops. Furthermore we explore some of the possibilities of combining relational and functional methods.