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

Displayed time zone: Eastern Time (US & Canada) change

16:00 - 18:00
Session 4FormaliSE at Sainte-Catherine
Chair(s): Stéphanie Challita Inria, France
Modular Synthesis of Verified Verifiers of Computation with STV Algorithms
Milad K. Ghale The Australian National University, Dirk Pattinson Australian National University, Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia
A Vision for Helping Developers Use APIs by Leveraging Temporal Patterns
Erick Raelijohn University of Montreal, Michalis Famelis Université de Montréal, Houari Sahraoui Université de Montréal
A Proof-Producing Translator for Verilog Development in HOL
Andreas Lööw Chalmers University of Technology, Magnus O. Myreen Chalmers University of Technology, Sweden
On the Formalization of Importance Measures using HOL Theorem Proving
Waqar Ahmad Carnegie Mellon University, Shahid Ali Murtza National University of Sciences and Technology, Osman Hasan Concordia University, Canada, Sofiene Tahar Concordia University
Day closing
C: Nico Plat Thanos