log in  |  register  |  feedback?  |  help
Logo
Analysis for Trustworthy Software
David Van Horn - Northeastern University
Tuesday, March 26, 2013, 11:00 am-12:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

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.

Bio

David Van Horn is a Research Assistant Professor at Northeastern University, where he works in the Programming Research Lab.  After receiving his PhD from Brandeis University in 2009, he was named a CRA Computing Innovation Fellow from 2009-2011.  His research concerns all aspects of program analysis and its applications to programming languages, software engineering, verification, and security.
Currently his work is supported by the National Science Foundation (NSF) and the Defense Advanced Research Projects Agency (DARPA).

This talk is organized by Adelaide Findlay