Bounded Verification of Voting Software

The authors 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 un-rollings. 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 nite model-finding. Their technique yields concrete counterexamples - traces of the procedure that violate the specification.