Verification of E-Voting Algorithms in Dafny
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866908731179008000 |
|---|---|
| author | Büttner, Robert Dießl, Fabian Franz Janoschek, Patrick Kostadinovic, Ivana Oback, Henrik Voß, Kilian Alber, Franziska Herrmann, Roland Möhle, Sibylle Rümmer, Philipp |
| author_facet | Büttner, Robert Dießl, Fabian Franz Janoschek, Patrick Kostadinovic, Ivana Oback, Henrik Voß, Kilian Alber, Franziska Herrmann, Roland Möhle, Sibylle Rümmer, Philipp |
| contents | Electronic voting procedures are implementations of electoral systems, making it possible to conduct polls or elections with the help of computers. This paper reports on the development of an open-source library of electronic voting procedures, which currently covers Score Voting, Instant-Runoff Voting, Borda Count, and Single Transferable Vote. The four procedures, of which two are discussed in detail, have been implemented in Dafny, formally verifying the consistency with functional specifications and key correctness properties. Using code extraction from the Dafny implementation, the library has been used to set up a voting web service. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_21084 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verification of E-Voting Algorithms in Dafny Büttner, Robert Dießl, Fabian Franz Janoschek, Patrick Kostadinovic, Ivana Oback, Henrik Voß, Kilian Alber, Franziska Herrmann, Roland Möhle, Sibylle Rümmer, Philipp Logic in Computer Science F.3.1; D.2.4 Electronic voting procedures are implementations of electoral systems, making it possible to conduct polls or elections with the help of computers. This paper reports on the development of an open-source library of electronic voting procedures, which currently covers Score Voting, Instant-Runoff Voting, Borda Count, and Single Transferable Vote. The four procedures, of which two are discussed in detail, have been implemented in Dafny, formally verifying the consistency with functional specifications and key correctness properties. Using code extraction from the Dafny implementation, the library has been used to set up a voting web service. |
| title | Verification of E-Voting Algorithms in Dafny |
| topic | Logic in Computer Science F.3.1; D.2.4 |
| url | https://arxiv.org/abs/2512.21084 |