BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/434
DTSTAMP:20230914T125924Z
SUMMARY:Human-in-the-Loop Embedded Systems: Specification\, Design\, and Ve
 rification
DESCRIPTION:Speaker: Dr. Sanjit A. Seshia (University of California\, Berke
 ley\nDepartment of Electrical Engineering and\nComputer Sciences\n253 Cora
 y Hall # 1770\nBerkeley\, CA 94720-1770\nUnited States of America)\n\nAbst
 ract: \nAbstract: Human interaction is central to many computing systems t
 hat require a high level of assurance. Examples of such systems include ai
 rcraft control systems (interacting with a pilot)\, automobiles with self-
 driving features (interacting with a driver)\, and medical devices (intera
 cting with a doctor or patient). The correctness of such systems depends n
 ot only on the autonomous controller\, but also on the actions of the huma
 n controller\, and\, critically\, on the interaction between the two.\n\nI
 n this talk\, I will present a formalism for human-in-the-loop embedded sy
 stems. I will then discuss the problem of synthesizing a semi-autonomous c
 ontroller from high-level specifications that expect occasional human inte
 rvention for correct operation. We present an algorithm for this problem\,
  and demonstrate its operation on problems related to driver assistance in
  automobiles. Finally\, I will present a data-driven approach to probabili
 stic modeling and verification of human driver behavior. Since probabilist
 ic models learned from data can suffer from estimation errors\, we have de
 signed and applied a new approach for model checking probabilistic models 
 with uncertainties. The talk will conclude with a broad survey of research
  challenges in this area.\n\nBio: Sanjit A. Seshia is an Associate Profess
 or in the Department of Electrical Engineering and Computer Sciences at th
 e University of California\, Berkeley. He received an M.S. and Ph.D. in Co
 mputer Science from Carnegie Mellon 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 logi
 c\, with a current focus on applying automated formal methods to problems 
 in embedded systems\, electronic design automation\, computer security\, a
 nd program analysis. His Ph.D. thesis work on the UCLID verifier and decis
 ion procedure helped pioneer the area of satisfiability modulo theories (S
 MT) and SMT-based verification. He is co-author of a widely-used textbook 
 on embedded systems. His awards and honors include a Presidential Early Ca
 reer Award for Scientists and Engineers (PECASE) from the White House\, an
  Alfred P. Sloan Research Fellowship\, the School of Computer Science Dist
 inguished Dissertation Award at Carnegie Mellon University\, and the inaug
 ural Prof. R. Narasimhan Lecture Award from TIFR.\n
URL:https://www.tcs.tifr.res.in/web/events/434
DTSTART;TZID=Asia/Kolkata:20140102T140000
DTEND;TZID=Asia/Kolkata:20140102T150000
LOCATION:D-460 (D-Block Conference Room)
END:VEVENT
END:VCALENDAR