Predicting physical properties, such as execution time or power, is central to the design of reliable embedded systems. However, the analysis of such properties is made difficult by their heavy dependence on the environment of the program, such as the processor it runs on. Modeling the environment by hand can be tedious, error-prone, and time consuming. In this talk, I will present a new, game-theoretic approach to estimating physical properties of software that is based on performing systematic measurements to automatically learn a model of the environment. We model the estimation problem as a game between our algorithm (player) and the environment of the program (adversary), where the player seeks to accurately predict program properties while the adversary sets environment parameters to thwart the player. I will present both theoretical and experimental evidence for the utility of our game-theoretic approach. On the theoretical side, for a range of properties on physical quantities such as time, we show that we can correctly predict these properties with probability greater than 1-delta by making a number of measurements that is polynomial in ln (1/delta) and the program size. Experimental results for execution time analysis demonstrate that our approach is efficient, effective, and highly portable.
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.