An Introduction to Voting Rule Verification
Bernhard Beckert, Thorsten Bormer, Rajeev Gore, Michael Kirsten,
Carsten Schürmann
In this chapter, we give an overview about the role that formal program
verification can play in social choice research. In particular, we focus on
one such technique, namely software bounded model checking (SBMC), which
statically analyses the implementation of a voting rule by exhaustively
looking for counterexamples in a finitely bounded search space. In order to
use a software bounded model checker, the voting rule implementation together
with the property to be shown are translated into a formula in propositional
or first-order logic before processing. The checker then tries to construct
either a proof or a counterexample, which can then be used to understand why
the voting rule violates the property.