关键词：电子投票机；设计；验证；测试
摘 要：This work incorporates and builds on previous research done jointly with Susmit Jha, Sanjit Seshia, and David Wagner on designing an electronic voting machine with the goal of verification of correctness.In that work we developed an approach of combining formal verification with user testing to verify an interactive machine and we demonstrated our technique with the design and implementation of a voting machine. This paper presents our work with a focus on the methodology and set of design principles we developed which made our approach possible. This also extends the functionality of our original voting machine to include a summary screen while still adhering to our methodology and design principles. We implement the new functionality and demonstrate that our original proof of correctness holds for the augmented voting machine.