Formal Methods for Dependable Computing: From Models, through Software, to Circuits
Lecture: Research Exchange | November 3 | 12-1 p.m. | Sutardja Dai Hall, Banatao Aud., 3rd floor
Sanjit A. Seshia, Asst. Professor of EECS, UC Berkeley
CITRIS (Ctr for Info Technology Research in the Interest of Society)
Live broadcast at mms://media.citris.berkeley.edu/webcast; Questions can be sent via Yahoo IM to username: citrisevents. The schedule for the fall Research Exchange is at http://www.citris-uc.org/events/RE-fall2010.
Abstract:
Computing has become ubiquitous and indispensable: it is embedded all
around us, in cell phones, automobiles, medical devices, and much
more. This ubiquity brings with it a growing challenge to ensure that
our computing infrastructure is also dependable and secure. We need to
develop and maintain complex software systems on top of increasingly
unreliable computing substrates under stringent resource constraints
such as energy usage.
In this talk, I will discuss how formal methods — mathematical
techniques for specification, design, and verification of systems —
can help improve system dependability. As illustrative case studies,
I will present work we have done on verifying timing properties of
control software (relevant for cyber-physical systems, such as
automobiles), analyzing the impact of faulty devices in digital
circuits, and designing electronic voting machines so as to enable
verification of desired properties. The talk will also touch upon some
of the core underlying technology, such as satisfiability modulo
theories (SMT) solvers, and describe challenges for the future.
Bio:
Sanjit A. Seshia is an assistant professor in the Department of
Electrical Engineering and Computer Sciences at the University of
California, Berkeley. He received an M.S. and a 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. He has received a
Presidential Early Career Award for Scientists and Engineers (PECASE),
an Alfred P. Sloan Research Fellowship, and the School of Computer
Science Distinguished Dissertation Award at Carnegie Mellon
University.
citriseditor@citris-uc.org, 510-643-4866
Available Now: Watch talk here on YouTube in Windows Media Player stream