CAREER: Foundations for Usable Program Analysis

Princeton University, Princeton NJ

Investigators

Abstract

Software pervades almost every aspect of the modern world, making software reliability a large and growing societal concern. Automated program-analysis and -verification technology aims to increase reliability, with minimal developer effort, by providing software developers with tools to answer questions about the behavior of their code. Since nearly all such questions are undecidable, progress in program-analysis technology over the last fifty years has been driven by heuristic reasoning techniques. These heuristics are often effective in practice, but they can be brittle and exhibit counter-intuitive behavior, making program analyzers to difficult to use. This project investigates the question: how can program-analysis tools be defined whose behavior can be understood and altered by software developers? This project builds foundations for usable program-analysis tools in order to deliver behavioral and performance guarantees that software developers may rely upon. It revisits three core program-analysis tasks -- numerical-invariant generation, termination analysis, and shape analysis -- and develops dependable reasoning principles to replace heuristics. The project contributes new program-analysis algorithms and new automated theorem-proving technology to support these analyses. By improving usability, the project aims to increase the scope and impact of program analysis, with the ultimate goal of creating better, more reliable software. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.