BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/144
DTSTAMP:20230914T125912Z
SUMMARY:On Voting Machine Design for Verification and Testability
DESCRIPTION:Speaker: Sanjit Seshia\nUniversity of California\, Berkeley\nDe
 partment of Electrical Engineering & Computer Sciences\n253 Cory\n\nAbstra
 ct: \nI will present an approach for the design and analysis of an electro
 nic voting machine based on a novel combination of formal verification and
  systematic testing by humans. The system was designed specifically to ena
 ble 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 int
 ended to work and formally verify that an implementation of our design mee
 ts this specification. However\, it is more challenging to verify that the
  composition of these components will behave as a voter would expect\, bec
 ause formalizing human expectations is difficult. We show how systematic t
 esting 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 conc
 lude with some observations on what we learned from this project and some 
 thoughts on how the ideas might generalize.\n\nBio: Available at http://ww
 w.eecs.berkeley.edu/~sseshia/bio.html\n
URL:https://www.tcs.tifr.res.in/web/events/144
DTSTART;VALUE=DATE:20101228
LOCATION:A-212 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR