Beckert, BernhardGore, RajeevSchurmann, Carsten2015-12-10July 17-19http://hdl.handle.net/1885/66190The ability to count ballots by computers allows us to design new voting schemes that are arguably fairer than existing schemes designed for hand-counting. We argue that formal methods can and should be used to ensure that such schemes behave as intendedKeywords: First order logic; Semantic criteria; Specification and verification; Voting schemes; Model checking; Semantics201310.1007/978-3-642-39185-9_22016-02-24