Abstract:

Work on software engineering, compiler optimization, program parallelization, system verification, and security assurance critically 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, such as Java, JavaScript, Python, Ruby, and many others, implying a growing need for precise and scalable program analyses for these languages.  For thirty years, the research community has expended a tremendous amount of effort designing effective analyses for such languages, but these past approaches, call for whole-program analyses, demand polynomial (or worse!)  resources, require complex constructions and correctness arguments, and are difficult to design and implement.

In this talk I will describe an alternative approach to analysis that meets the scalability challenge of modern systems.  I will show 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 program components.

This work traces an arc of research that began with a very theoretical investigation of existing program analyses and developed into a new practical approach to the design of analysis and verification tools for higher-order program languages. To conclude, I will show how I am applying this approach to vet the security of Android applications.