Seminars

Specification Mining for Controller Verification and Synthesis PDF
Sanjit Seshia, Dept. of Electrical Engineering and Computer Science, University of California, Berkeley

5/22/2013, 4:00pm, GHC 8102

Abstract

Writing a formal specification is a crucial first step for formal verification and correct-by-construction synthesis. However, in practice, one often does not have a specification that captures all relevant system properties. This inadequacy in specification can result in missed bugs and failed attempts at synthesis.

In this talk, I will present our recent work in mining specifications for controller verification and synthesis. First, I will describe our work on synthesizing specifications for closed-loop control models. We generate properties in signal temporal logic and show how this can find subtle bugs in industrial automotive controllers written in a language such as Simulink. Our approach combines SMT solving and simulation-based verification in a counterexample-guided loop. Next, I will describe work on generating environment assumptions for synthesis of finite-state transducers from temporal logic. This approach is "counterstrategy-guided," combining model checking with learning based on version spaces. Both projects are based on a common theme of combining deductive formal methods with inductive learning from examples.

Biography

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

http://www.eecs.berkeley.edu/~sseshia/