Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Mon 27 May 2019 16:00 - 16:25 at Sainte-Catherine - Session 4 Chair(s): Stéphanie Challita

Single transferrable vote (STV) is a family of preferential voting systems, different instances of which are used in binding elections throughout the world. We give a formal specification of this family, from which we derive fully verified tools that verify the computation for various instances of STV vote counting. These tools validate the probably correct execution of a run of a vote counting algorithm, based on a transcript of the count.

Our framework distils the similarities and differences of various instances of STV and gives a uniform and modular way of synthesising verifiers for its various instances, and provides the flexibility and ease for adapting and extending it to a variety of STV schemes. We minimise the trusted base in correctness of the tools produced by using the HOL4 and CakeML as the technical basis. We first formally specify and verify the tools in HOL4 and then obtain the machine executable versions for the tools by relying on the verified proof translator and the compiler of the CakeML. Moreover, proofs that we establish in HOL4 and CakeML are almost completely automated so that new verified instances of STV can be created with no (or minimal) extra proof. Finally, our experimental results with executable code demonstrate feasibility of deploying the framework for verifying real size elections having an STV counting algorithm.

Mon 27 May

Formalise-2019-papers
16:00 - 18:00: FormaliSE 2019 - Session 4 at Sainte-Catherine
Chair(s): Stéphanie ChallitaInria, France
Formalise-2019-papers16:00 - 16:25
Full-paper
Milad K. GhaleThe Australian National University, Dirk PattinsonAustralian National University, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia
Formalise-2019-papers16:25 - 16:40
Short-paper
Erick RaelijohnUniversity of Montreal, Michalis FamelisUniversité de Montréal, Houari SahraouiUniversité de Montréal
Formalise-2019-papers16:40 - 17:05
Full-paper
Andreas LööwChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Sweden
Formalise-2019-papers17:05 - 17:30
Full-paper
Waqar AhmadCarnegie Mellon University, Shahid Ali MurtzaNational University of Sciences and Technology, Osman HasanConcordia University, Canada, Sofiene TaharConcordia University
Formalise-2019-papers17:30 - 18:00
Day closing
Nico PlatThanos