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

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Konferenceartikel › Forskning › 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

Originalsprog	Engelsk
Tidsskrift	Karlsruhe Reports in Informatics
Vol/bind	2010
Udgave nummer	13
Sider (fra-til)	235-252
Antal sider	17
ISSN	2190-4782
Status	Udgivet - 2010
Begivenhed	International Conference on Formal Verification of Object-Oriented Software - Paris, Frankrig Varighed: 28 jun. 2010 → 30 jun. 2010 http://foveoos2010.cost-ic0701.org/

Konference

Konference	International Conference on Formal Verification of Object-Oriented Software
Land/Område	Frankrig
By	Paris
Periode	28/06/2010 → 30/06/2010
Internetadresse	http://foveoos2010.cost-ic0701.org/

Emneord

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

Adgang til dokumentet

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

Verifiable Elections
Kiniry, J. R. (PI) & Cochran, D. (PI)
01/01/2010 → 01/01/2012
Projekter: Projekt › Forskning

Citationsformater

@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

Konference

Emneord

Adgang til dokumentet

Fingeraftryk

Projekter

Verifiable Elections

Citationsformater