Tata Institute of Fundamental Research
On Voting Machine Design for Verification and Testability
Seminar
Speaker:
Sanjit Seshia
University of California, Berkeley
Department of Electrical Engineering & Computer Sciences
253 Cory
Date:
Tuesday, 28 Dec 2010 (all day)
Venue:
A-212 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
I will present an approach for the design and analysis of an electronic voting machine based on a novel combination of formal verification and systematic testing by humans. The system was designed specifically to enable verification and testing. In our architecture, the voting machine is a finite-state transducer that implements the bare essentials required for an election. We formally specify how each component of the machine is intended to work and formally verify that an implementation of our design meets this specification. However, it is more challenging to verify that the composition of these components will behave as a voter would expect, because formalizing human expectations is difficult. We show how systematic testing by humans can be used to address this issue, and in particular to verify that the machine will behave correctly on election day. I will conclude with some observations on what we learned from this project and some thoughts on how the ideas might generalize.
Bio: Available at http://www.eecs.berkeley.edu/~sseshia/bio.html
| Speaker: | Sanjit Seshia University of California, Berkeley Department of Electrical Engineering & Computer Sciences 253 Cory |
| Date: | Tuesday, 28 Dec 2010 (all day) |
| Venue: | A-212 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
I will present an approach for the design and analysis of an electronic voting machine based on a novel combination of formal verification and systematic testing by humans. The system was designed specifically to enable verification and testing. In our architecture, the voting machine is a finite-state transducer that implements the bare essentials required for an election. We formally specify how each component of the machine is intended to work and formally verify that an implementation of our design meets this specification. However, it is more challenging to verify that the composition of these components will behave as a voter would expect, because formalizing human expectations is difficult. We show how systematic testing by humans can be used to address this issue, and in particular to verify that the machine will behave correctly on election day. I will conclude with some observations on what we learned from this project and some thoughts on how the ideas might generalize.
Bio: Available at http://www.eecs.berkeley.edu/~sseshia/bio.html
Bio: Available at http://www.eecs.berkeley.edu/~sseshia/bio.html