Quantitative Verification of Embedded Software

Abstract:

Embedded systems tightly integrate computation with physical processes. Thus, the verification of embedded software often requires the estimation of physical quantities, such as timing and energy consumption, that are affected both by the software and by its environment. A major challenge for such verification is the difficulty of accurate environment modeling. I will discuss the challenges using illustrative examples, and present a new approach to this problem based on the combination of inductive inference (learning from examples) with deductive reasoning. I will present a concrete instance of this approach for timing analysis in a system called GameTime.

Presentation Slides

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 program analysis. 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.