Seminars

Integrating Induction and Deduction for Verification and Synthesis

Christel Baier, Professor
Technische Universität Dresden , Germany

05/21/2010, 2pm, GHC-6501

Abstract

Even with 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 approach integrates techniques such as satisfiability solving and theorem proving (SAT/SMT), game-theoretic online learning, learning polyhedra, numerical simulation, and fixpoint computation.  I will illustrate this combination of inductive and deductive methods for three problems: (i) the synthesis of switching logic for hybrid systems; (ii) program synthesis applied to malware deobfuscation, and (iii) the verification of execution time properties of embedded software.

 

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