Seminars

Integrating Induction and Deduction for Verification and Synthesis

Thursday, April 15, 2010

Prof. Sanjit Seshia

Abstract

Despite impressive advances in formal methods over the last few decades, some problems in automatic verification and synthesis remain challenging. Examples include the analysis and synthesis of hybrid systems with non-linear dynamics, and the verification of quantitative properties of software such as execution time. In this talk, I will present a new approach to automatic verification and synthesis based on a combination of inductive methods (learning from examples), and deductive methods (based on logical inference and abstraction). Our methods combine techniques such as satisfiability solving and theorem proving (SAT/SMT), learning polyhedra, numerical simulation, and fixpoint computation. I will illustrate this combination of inductive and deductive methods for three problems: (i) the synthesis of hybrid automata with non-linear dynamics; (ii) program synthesis applied to malware deobfuscation, and (iii) the verification of execution time properties of embedded software.

Speaker Biography

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 computer security, electronic design automation, 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.