Rajeev Gore

Interactive Synthesis of Verified Vote-counting Programs

VCLA hosted a talk by Rajeev Gore

DATE:Wednesday, September 26, 2018
TIME:16:30 s.t.
VENUE:Seminar Room Gödel, Favoritenstrasse 9-11, Ground Floor, (HB EG 10)


Single-transferable (preferential) voting (STV) allows a voter to create a ballot by listing the C candidates in decreasing order of preference in an election for V vacant seats. Counting such preferential ballots is extremely complicated and there are many slightly different variations of STV counting. I will show how we have used the interactive theorem prover Coq to generate a computer program to implement various versions of STV counting. The program is efficient and is guaranteed to be correct with respect to its specification. The talk is a product of the joint work with Dirk Pattinson, Milad Ghale and Mukesh Tiwari.

Comments are closed.