ICS Seminar: Prof. Sanjit Seshia
Prof. Sanjit Seshia
UC Berkeley
Thursday, April 15, 2:00pm, ENS 637
Integrating Induction and Deduction for Verification and Synthesis
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.