Human interaction is central to many computing systems that require a high level of assurance. We term such systems as "high-confidence interactive systems". Examples include aircraft control systems (interacting with a pilot), 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 system 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 human operator.
In this talk, I will describe an approach that addresses these challenges by combining algorithmic methods with systematic and efficient human-driven interventions and testing. For instance, one can verify the correctness of such interactive systems by combining algorithmic, formal 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 with 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 ideas form first steps towards the design of dependable interactive systems. The talk will conclude with directions for future work.
Brief Biography:
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 program analysis. 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, and the School of Computer Science Distinguished Dissertation Award at Carnegie Mellon University.
