Login
Talks & Seminars
Title: Human-in-the-Loop Embedded Systems: Specification, Design and Verification
Prof. Sanjit A. Seshia, University of California, Berkeley
Date & Time: January 7, 2014 14:40
Venue: Conference Room, C Block, 01st Floor, Department of Computer Science and Engineering, Kanwal Rekhi Building
Abstract:
Human interaction is central to many computing systems that require a high level of assurance. Examples of such systems include aircraft control systems (interacting with a pilot), automobiles with self-driving features (interacting with a driver), and medical devices (interacting with a doctor, nurse, or patient). The correctness of such systems depends not only on the autonomous controller, but also on the actions of the human controller, and, critically, on the interaction between the two. In this talk, I will present a formalism for human-in-the-loop embedded systems. I will also discuss the problem of synthesizing a semi-autonomous controller from high-level specifications that expect occasional human intervention 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 probabilistic modeling and verification of human driver behavior. Since probabilistic models learned from data can suffer from estimation errors, we have designed and applied a new approach for model checking probabilistic models with uncertainties. The talk will conclude with a brief overview of research challenges in this area.
Speaker Profile:
Sanjit A. Seshia is an Associate Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer 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 logic, with a current focus on applying automated formal methods to problems in embedded systems, electronic design automation, computer security, and synthetic biology. His Ph.D. thesis work on the UCLID verifier and decision procedure helped pioneer the area of satisfiability modulo theories (SMT) and SMT-based verification. He is co-author of a widely-used textbook on embedded systems. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE) from the White House, an Alfred P. Sloan Research Fellowship, the School of Computer Science Distinguished Dissertation Award at Carnegie Mellon University, and the inaugural Prof. R. Narasimhan Lecture Award from TIFR, India.
List of Talks

Webmail

Username:
Password:
Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback