Engineering Software for Modular Formalisation and Verification of STV Algorithms

被引：0
|
作者：
Ghale, Milad K. [1 ]
机构：
[1] Australian Natl Univ, Res Sch Comp Sci, Canberra, ACT, Australia
来源：
FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2018 | 2018年 / 11232卷
关键词：
D O I：
10.1007/978-3-030-02450-5_35
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
We introduce new software for provably correct computation with Single Transferable Voting (STV) algorithms. The software is engineered as a framework for modular formalisation, verification, extraction of executable certifying programmes, and verified certificate checking for various STV algorithms. We demonstrate functionality and effectiveness of our approach by evaluating the software on some real-size elections.
引用
收藏
页码：459 / 463
页数：5
相关论文
共 50 条
  • [1] Modular Formalisation and Verification of STV Algorithms
    Ghale, Milad K.
    Gore, Rajeev
    Pattinson, Dirk
    Tiwari, Mukesh
    [J]. ELECTRONIC VOTING, 2018, 11143 : 51 - 66
  • [2] Engineering and Employing Reusable Software Components for Modular Verification
    Welch, Daniel
    Sitaraman, Murali
    [J]. MASTERING SCALE AND COMPLEXITY IN SOFTWARE REUSE (ICSR 2017), 2017, 10221 : 139 - 154
  • [3] Modular Synthesis of Verified Verifiers of Computation with STV Algorithms
    Ghale, Milad K.
    Pattinson, Dirk
    Norrish, Michael
    [J]. 2019 IEEE/ACM 7TH INTERNATIONAL WORKSHOP ON FORMAL METHODS IN SOFTWARE ENGINEERING (FORMALISE 2019), 2019, : 85 - 94
  • [4] Modular verification of software components in C
    Chaki, S
    Clarke, E
    Groce, A
    Jha, S
    Veith, H
    [J]. 25TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, PROCEEDINGS, 2003, : 385 - 395
  • [5] Modular verification of software components in C
    Chaki, S
    Clarke, EM
    Groce, A
    Jha, S
    Veith, H
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2004, 30 (06) : 388 - 402
  • [6] Towards Static Modular Software Verification
    Department of Software Engineering, Technische Universität Berlin, Ernst-Reuter-Platz 7, Berlin
    10587, Germany
    [J]. Lect. Notes Informatics (LNI), Proc. - Series Ges. Inform. (GI), (147-153):
  • [7] Modular Verification of Interrupt-Driven Software
    Sung, Chungha
    Kusano, Markus
    Wang, Chao
    [J]. PROCEEDINGS OF THE 2017 32ND IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE'17), 2017, : 206 - 216
  • [8] The influence of software module systems on modular verification
    Li, HC
    Fisler, K
    Krishnamurthi, S
    [J]. MODEL CHECKING SOFTWARE, PROCEEDINGS, 2002, 2318 : 60 - 78
  • [9] SOFTWARE ENGINEERING OF THE FLOW ALGORITHMS
    Panyukov, A. V.
    Teleghin, V. A.
    [J]. BULLETIN OF THE SOUTH URAL STATE UNIVERSITY SERIES-MATHEMATICAL MODELLING PROGRAMMING & COMPUTER SOFTWARE, 2008, (02): : 78 - 99
  • [10] Software verification and software engineering a practitioner's perspective
    Hall, Anthony
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 70 - 73
12345