Votail: A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections

Dermot Robert  Cochran; Joseph Roland Kiniry

Votail: A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections

Dermot Robert Cochran
, Joseph Roland Kiniry

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

Abstract

Votail is an open source Java implementation of Irish Proportional Representation by Single Transferable Vote (PR-STV). Its functional requirements, derived from Irish electoral law, are formally specified using the Business Object Notation (BON) and refined to a Java Modeling Language (JML) specification. Formal methods are used to verify and validate the correctness of the software. This is the first public release of a formally verified PR-STV open source system for ballot counting and the most recent of only about half a dozen releases of formally verified e-voting software

Original language	English
Journal	Karlsruhe Reports in Informatics
Volume	2010
Issue number	13
Pages (from-to)	235-252
Number of pages	17
ISSN	2190-4782
Publication status	Published - 2010
Event	International Conference on Formal Verification of Object-Oriented Software - Paris, France Duration: 28 Jun 2010 → 30 Jun 2010 http://foveoos2010.cost-ic0701.org/

Conference

Conference	International Conference on Formal Verification of Object-Oriented Software
Country/Territory	France
City	Paris
Period	28/06/2010 → 30/06/2010
Internet address	http://foveoos2010.cost-ic0701.org/

Keywords

Votail
Proportional Representation
Single Transferable Vote
Formal Verification
E-Voting Software

Access to Document

http://www.kindsoftware.com/documents/published/CochranKiniry10.pdf

Verifiable Elections
Kiniry, J. R. (PI) & Cochran, D. (PI)
01/01/2010 → 01/01/2012
Project: Research

Cite this

@inproceedings{fdee55001a4b44069d18dadef0bbdb45,

title = "Votail: A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections",

abstract = "Votail is an open source Java implementation of Irish Proportional Representation by Single Transferable Vote (PR-STV). Its functional requirements, derived from Irish electoral law, are formally specified using the Business Object Notation (BON) and refined to a Java Modeling Language (JML) specification. Formal methods are used to verify and validate the correctness of the software. This is the first public release of a formally verified PR-STV open source system for ballot counting and the most recent of only about half a dozen releases of formally verified e-voting software",

keywords = "Votail, Proportional Representation, Single Transferable Vote, Formal Verification, E-Voting Software, Votail, Proportional Representation, Single Transferable Vote, Formal Verification, E-Voting Software",

author = "Cochran, \{Dermot Robert\} and Kiniry, \{Joseph Roland\}",

note = "Ser ud til at v{\ae}re publiceret i proceedings of FoVeOOS 2010, Karlsruhe Reports in Informatics 2010,13, Edited by Karlsruhe Institute of Technology, Faculty of Informatics ISSN 2190-4782. - Jens Chr. 11.03.11 {\AE}ndret til konf.bidrag i n{\ae}vnte tidsskrift - Alex 17.03.11; International Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2010 ; Conference date: 28-06-2010 Through 30-06-2010",

year = "2010",

language = "English",

volume = "2010",

pages = "235--252",

journal = "Karlsruhe Reports in Informatics",

issn = "2190-4782",

publisher = "Karlsruhe Institute of Technology",

number = "13",

url = "http://foveoos2010.cost-ic0701.org/",

}

TY - GEN

T1 - Votail: A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections

AU - Cochran, Dermot Robert

AU - Kiniry, Joseph Roland

N1 - Ser ud til at være publiceret i proceedings of FoVeOOS 2010, Karlsruhe Reports in Informatics 2010,13, Edited by Karlsruhe Institute of Technology, Faculty of Informatics ISSN 2190-4782. - Jens Chr. 11.03.11 Ændret til konf.bidrag i nævnte tidsskrift - Alex 17.03.11

PY - 2010

Y1 - 2010

N2 - Votail is an open source Java implementation of Irish Proportional Representation by Single Transferable Vote (PR-STV). Its functional requirements, derived from Irish electoral law, are formally specified using the Business Object Notation (BON) and refined to a Java Modeling Language (JML) specification. Formal methods are used to verify and validate the correctness of the software. This is the first public release of a formally verified PR-STV open source system for ballot counting and the most recent of only about half a dozen releases of formally verified e-voting software

AB - Votail is an open source Java implementation of Irish Proportional Representation by Single Transferable Vote (PR-STV). Its functional requirements, derived from Irish electoral law, are formally specified using the Business Object Notation (BON) and refined to a Java Modeling Language (JML) specification. Formal methods are used to verify and validate the correctness of the software. This is the first public release of a formally verified PR-STV open source system for ballot counting and the most recent of only about half a dozen releases of formally verified e-voting software

KW - Votail

KW - Proportional Representation

KW - Single Transferable Vote

KW - Formal Verification

KW - E-Voting Software

KW - Votail

KW - Proportional Representation

KW - Single Transferable Vote

KW - Formal Verification

KW - E-Voting Software

M3 - Conference article

SN - 2190-4782

VL - 2010

SP - 235

EP - 252

JO - Karlsruhe Reports in Informatics

JF - Karlsruhe Reports in Informatics

IS - 13

T2 - International Conference on Formal Verification of Object-Oriented Software

Y2 - 28 June 2010 through 30 June 2010

ER -

Votail: A Formally Specified and Verified Ballot Counting System for Irish PR-STV Elections

Abstract

Conference

Keywords

Access to Document

Fingerprint

Projects

Verifiable Elections

Cite this