Skip to content
Joseph R. Kiniry edited this page Mar 6, 2013 · 1 revision

A Logic-Based System for Analysing Vote Counting Algorithms And its Application to the CADE Election System Bernhard Beckert, Rajeev Gore, and Carsten Schürmann

We present a logic-based system for analysing vote counting algorithms, Similar to model checking approaches, the system can gen- erate examples for erratic behaviour. It uses a Celf linear-logic program describing the voting algorithm and a specification in first-order logic. As a case study, we have applied our system to the vote counting algo- rithm that is used in the CADE Trustees Elections. We found the CADE algorithm to strictly differ from the standard. It is a misnomer to say that the CADE algorithm implements a Single Transferable Vote system.

Clone this wiki locally