Tata Institute of Fundamental Research
A Theory of Algorithmic Improvisation
STCS Seminar
Speaker:
Sanjit A. Seshia (University of California at Berkeley
Department of Electrical Engineering
and Computer Sciences
253 Cory Hall
Berkeley, CA 94720-1770
United States of Anerica
)
Organiser:
Prahladh Harsha
Date:
Monday, 11 Jan 2016, 11:00 to 12:00
Venue:
A-212 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
Abstract: Improvisation is often described as "acting without preparation", with an element of randomness. Can an algorithm improvise? What does it mean for an algorithm to improvise? What applications can benefit from algorithmic improvisation?
In this talk, I will explore these questions by presenting "control improvisation", a formalization of the notion of algorithmic improvisation. A simple form of control improvisation is to find a random generator of strings from a formal language satisfying certain hard, soft, and randomness requirements. Applications of control improvisation are surprisingly diverse, ranging from robotics to software testing to computational music. I will present the theory of control improvisation, an analysis of its computational complexity, and some preliminary applications that we have explored at Berkeley.
Bio: 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 cyber-physical systems, computer security, electronic design automation, 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 textbook on embedded systems used in more than 50 countries and has led the development of technologies for cyber-physical systems education based on formal methods. 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.
| Speaker: | Sanjit A. Seshia (University of California at Berkeley Department of Electrical Engineering and Computer Sciences 253 Cory Hall Berkeley, CA 94720-1770 United States of Anerica ) |
| Organiser: | Prahladh Harsha |
| Date: | Monday, 11 Jan 2016, 11:00 to 12:00 |
| Venue: | A-212 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
Abstract: Improvisation is often described as "acting without preparation", with an element of randomness. Can an algorithm improvise? What does it mean for an algorithm to improvise? What applications can benefit from algorithmic improvisation?
In this talk, I will explore these questions by presenting "control improvisation", a formalization of the notion of algorithmic improvisation. A simple form of control improvisation is to find a random generator of strings from a formal language satisfying certain hard, soft, and randomness requirements. Applications of control improvisation are surprisingly diverse, ranging from robotics to software testing to computational music. I will present the theory of control improvisation, an analysis of its computational complexity, and some preliminary applications that we have explored at Berkeley.
Bio: 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 cyber-physical systems, computer security, electronic design automation, 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 textbook on embedded systems used in more than 50 countries and has led the development of technologies for cyber-physical systems education based on formal methods. 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.
In this talk, I will explore these questions by presenting "control improvisation", a formalization of the notion of algorithmic improvisation. A simple form of control improvisation is to find a random generator of strings from a formal language satisfying certain hard, soft, and randomness requirements. Applications of control improvisation are surprisingly diverse, ranging from robotics to software testing to computational music. I will present the theory of control improvisation, an analysis of its computational complexity, and some preliminary applications that we have explored at Berkeley.
Bio: 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 cyber-physical systems, computer security, electronic design automation, 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 textbook on embedded systems used in more than 50 countries and has led the development of technologies for cyber-physical systems education based on formal methods. 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.