Interactive Synthesis of Verified Vote-counting Programs

VCLA hosted a talk by Rajeev Gore

ABSTRACT

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.