Home

Program

Call for Papers

Submissions

9th ACM SIGPLAN-SIGSOFT Workshop on
Program Analysis for Software Tools and Engineering (PASTE)

June 5 - 6, 2010
Toronto, Canada
Co-located with PLDI 2010


Sponsored by    ACM SIGPLAN ACM SIGSOFT

Keynote for Saturday June 5th

Speaker

Jeff Foster (University of Maryland)

Program Analysis, Understanding, and Synthesis with Symbolic Execution

Symbolic execution, first proposed more than 30 years ago as an approach to enhanced testing, has received significant recent attention as a bug finding technique. When used for bug finding, symbolic execution is applied heuristically to search a small portion of the program's execution space. In this talk, I will discuss our progress on pushing symbolic execution beyond bug finding, towards new program analysis, understanding, and synthesis applications. I will describe four projects under way: (1) An empirical analysis of software configuration spaces, using symbolic execution as an empirical apparatus; (2) A project to check web application security using symbolic execution; (3) A new system that mixes precise symbolic execution with coarse type-based static analysis; and (4) A program synthesis tool that uses symbolic execution to automatically create program inverses. All of these projects take advantage of the strengths of symbolic execution---fully precise execution with minimal abstraction---while side-stepping performance and tractability limitations. Ultimately, I expect that judicious use of symbolic execution will be a key component in many of the program analysis, understanding, and synthesis tools of the future.

Biography

Jeff Foster is an Associate Professor in the Department of Computer Science at the University of Maryland, College Park. He received his Ph.D. in Computer Science from the University of California, Berkeley, and he received M.Eng. and B.S. degrees from Cornell University, also in Computer Science. Jeff's research aims to develop programming language technology to solve software engineering problems. His current focus is on symbolic execution, analysis of dynamic scripting languages, dynamic software updating, and program synthesis.