| abstract |
 |
 |
 |
Work on software engineering, compiler optimizations, program parallelization, system verification, and security assurance depends on program analysis, a ubiquitous and central theme of programming language research. At the same time, the production of modern software systems employs expressive, higher-order programming languages, e.g., Java, JavaScript, Python, Ruby, etc., implying a growing need for fast, precise, and scalable higher-order program analyses.
For thirty years, the research community has expended a tremendous amount of effort designing effective, scalable analysis for higher-order programming languages. These past approaches, however, call for whole-program analyses, demand polynomial (or worse!) resources, and require complex constructions and correctness arguments. In this talk I will describe how these limitations can be overcome and provide new insights into the potential of higher-order program analysis. These ideas enable a new approach to analysis that meets the scalability challenge of modern systems. I will sketch how to leverage these new ideas in order to create a straightforward derivation process, thereby lowering verification costs, accommodating sophisticated language features and program properties, and reasoning about modular, i.e., incomplete, programs. In the long run, my foundational results should open several new directions for program analysis and its applications, and I will conclude my talk with a sketch of these possibilities. |