Functional Verification and Information Flow Analysis of an Electronic Voting System

@incollection{GrahlScheben2016,
  author    = {Daniel Grahl and Christoph Scheben},
  title     = {Functional Verification and Information Flow Analysis of an Electronic Voting System},
  booktitle = {Deductive Software Verification - The {\KeY} Book: From Theory to Practice},
  year      = {2016},
  publisher = {Springer},
  pages     = {593--607},
  chapter   = {18},
  part      = {V: Case Studies},
  doi       = {10.1007/978-3-319-49812-6_18},
  series    = {Lecture Notes in Computer Science},
  volume    = {10001},
  month     = dec,
  abstract  = {Electronic voting (e-voting) systems that are used in public elections need to fulfill
               a broad range of strong requirements concerning both safety and security. Among those
               requirements are reliability, robustness, privacy of votes, coercion resistance, and
               universal verifiability. Bugs in or manipulations of an e-voting system can have
               considerable influence on society. Therefore, e-voting systems are an obvious target
               for software verification. This case study proves the preservation of privacy of votes
               for a basic electronic voting system. Altogether the considered code comprises eight
               classes and thirteen methods in about 150 lines of code of a rich fragment of Java.}
}