Reasoning About Vote Counting Schemes Using Light-Weight and Heavy-Weight Methods

Bernhard Beckert, Thorsten Bormer, Rajeev Gor\'e, Michael Kirsten, and Thomas Meumann


We compare and contrast our experiences in specifying, implementing
and verifying the monotonicity property of a simple plurality voting
scheme using modern light-weight and heavy-weight verification tools.