Verification by, for, and of Humans: Cyber-Physical Systems and Beyond
Department of Electrical Engineering and Computer Sciences
University of California, Berkeley
Abstract:
Algorithmic formal methods for specification, verification, and synthesis have made impressive advances over recent decades. Even so, it can be challenging for non-expert human users to succeed with formal methods in practice. In this talk, I will describe three lines of work concerning the verification by, for, and of humans: (1) reducing the formal specification "burden" for users of verification tools; (2) impacting large-scale engineering education with formal methods, and (3) incorporating formal methods into the design process for next-generation human-in-the-loop systems. Central to all three projects is an approach based on the integration of induction (learning from examples) with deduction (logical inference and constraint solving). Theory and techniques will be illustrated with applications from the domain of cyber-physical systems including automotive control systems, online virtual laboratories, and semi-autonomous driving.
Biodata:
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 cyber-physical systems, computer security, electronic design automation, 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 and has led the development of technologies for cyber-physical systems education based on formal methods. 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.