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.