BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/333
DTSTAMP:20230914T125920Z
SUMMARY:Designing High-Confidence Interactive Systems: Electronic Voting\, 
 Self-Driving Cars\, and Beyond
DESCRIPTION:Speaker: Sanjit A. Seshia (University of California\, Berkeley\
 nDepartment of Electrical Engineering and Computer Science\n253 Coray Hall
  #1770\nBerkeley\, CA 94720-1770\nUnited States of America)\n\nAbstract: \
 nHuman interaction is central to many computing systems that require a hig
 h level of assurance. We term such systems as "high-confidence interactive
  systems". Examples include aircraft control systems (interacting with a p
 ilot)\, automobiles with self-driving features (interacting with a driver)
 \, medical devices (interacting with a doctor or patient)\, and electronic
  voting machines (interacting with a voter). In order to ensure that these
  systems are designed correctly\, one must model and analyze the entire sy
 stem including the human in the loop. This is challenging for at least two
  reasons: (i) it is difficult to obtain an accurate mathematical model of 
 human operators\, and (ii) the design of such a system must systematically
  and judiciously divide control between an autonomous program and the huma
 n operator.\n\nIn this talk\, I will describe an approach that addresses t
 hese challenges by combining algorithmic methods with systematic and effic
 ient human-driven interventions and testing. For instance\, one can verify
  the correctness of such interactive systems by combining algorithmic\, fo
 rmal verification with systematic testing by humans. I will illustrate the
  application of this idea to electronic voting in the U.S. Similarly\, for
  systems that operate in both manual and autonomous modes\, such as cars w
 ith self-driving features\, one can automatically synthesize the code for 
 autonomous operation that is correct by construction along with conditions
  that require minimal interventions by a human driver. Together these idea
 s form first steps towards the design of dependable interactive systems. T
 he talk will conclude with directions for future work.\n\nBrief Biography:
 \n\nSanjit A. Seshia is an Associate Professor in the Department of Electr
 ical Engineering and Computer Sciences at the University of California\, B
 erkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie M
 ellon University\, and a B.Tech. in Computer Science and Engineering from 
 the Indian Institute of Technology\, Bombay. His research interests are in
  dependable computing and computational logic\, with a current focus on ap
 plying automated formal methods to problems in embedded systems\, electron
 ic design automation\, computer security\, and program analysis. His Ph.D.
  thesis work on the UCLID verifier and decision procedure helped pioneer t
 he area of satisfiability modulo theories (SMT) and SMT-based verification
 . He is co-author of a widely-used textbook on embedded systems. His award
 s and honors include a Presidential Early Career Award for Scientists and 
 Engineers (PECASE) from the White House\, an Alfred P. Sloan Research Fell
 owship\, and the School of Computer Science Distinguished Dissertation Awa
 rd at Carnegie Mellon University.\n
URL:https://www.tcs.tifr.res.in/web/events/333
DTSTART;TZID=Asia/Kolkata:20130109T160000
DTEND;TZID=Asia/Kolkata:20130109T170000
LOCATION:AG-66 (Lecture Theatre)
END:VEVENT
END:VCALENDAR