%0 Book Section %1 dennis_08_bounded %A Dennis, Greg %A Yessenov, Kuat %A Jackson, Daniel %D 2008 %J Verified Software: Theories, Tools, Experiments %K 2008 bounded_verification %P 130--145 %R http://dx.doi.org/10.1007/978-3-540-87873-5_13 %T Bounded Verification of Voting Software %U http://dx.doi.org/10.1007/978-3-540-87873-5_13 %X We present a case-study in which vote-tallying software is analyzed using a bounded verification technique, whereby all executions of a procedure are exhaustively examined within a finite space given by a bound on the size of the heap and the number of loop unrollings. The technique involves an encoding of the procedure in an intermediate relational programming language, a translation of that language to relational logic, and an analysis of the logic that exploits recent advances in finite model-finding. Our technique yields concrete counterexamples – traces of the procedure that violate the specification. The vote-tallying software, used for public elections in the Netherlands, had previously been annotated with specifications in the Java Modeling Language and analyzed with ESC/Java2. Our analysis found counterexamples to the JML contracts, indicating bugs in the code and errors in the specifications that evaded prior analysis.

@incollection{dennis_08_bounded, abstract = {We present a case-study in which vote-tallying software is analyzed using a bounded verification technique, whereby all executions of a procedure are exhaustively examined within a finite space given by a bound on the size of the heap and the number of loop unrollings. The technique involves an encoding of the procedure in an intermediate relational programming language, a translation of that language to relational logic, and an analysis of the logic that exploits recent advances in finite model-finding. Our technique yields concrete counterexamples – traces of the procedure that violate the specification. The vote-tallying software, used for public elections in the Netherlands, had previously been annotated with specifications in the Java Modeling Language and analyzed with ESC/Java2. Our analysis found counterexamples to the JML contracts, indicating bugs in the code and errors in the specifications that evaded prior analysis.}, added-at = {2009-02-11T20:13:02.000+0100}, author = {Dennis, Greg and Yessenov, Kuat and Jackson, Daniel}, biburl = {https://www.bibsonomy.org/bibtex/29b9681fc36c58273713c8829e1efebdf/leonardo}, citeulike-article-id = {3440424}, doi = {http://dx.doi.org/10.1007/978-3-540-87873-5_13}, interhash = {ee4b47416386c01c8ca5b9c63224f500}, intrahash = {9b9681fc36c58273713c8829e1efebdf}, journal = {Verified Software: Theories, Tools, Experiments}, keywords = {2008 bounded_verification}, pages = {130--145}, posted-at = {2008-10-22 15:05:16}, priority = {2}, timestamp = {2009-02-11T20:13:02.000+0100}, title = {Bounded Verification of Voting Software}, url = {http://dx.doi.org/10.1007/978-3-540-87873-5_13}, year = 2008 }