CAREER: Program Analysis with Precise Abstractions

Program analysis techniques reason about program behavior and have been widely used in software testing, bug finding, and quality assurance. In general, the problem of static program analysis is undecidable. Practical program analyses typically over-approximate program semantics via imprecise abstractions. This project will devise precise program abstractions based on graph theory to make program analysis techniques more reliable and usable. The project's novelties are (1) providing a unified theory of precise abstractions that can be used to design more principled analysis techniques with formal guarantees and (2) enabling more scalable program analysis frameworks for tackling practical analysis problems in emerging areas. The project's impacts are (1) increasing the capability of building reliable software, (2) leading to more reliable and usable program analysis frameworks for analyzing software artifacts, and (3) advocating the fundamental concept of abstraction in computing. The goal of this project is to explore theoretical developments and practical techniques centered around the InterDyck graph abstraction. It focuses on developing a systematic framework to precisely model program semantics and devise practical algorithms for solving the reachability problem based on the InterDyck graph abstraction. This project explores three main directions: (1) understanding the expressiveness and limitations of the InterDyck graph abstraction; (2) developing efficient demand-driven and exhaustive analysis algorithms for InterDyck-reachability; and (3) promoting an integrated educational approach to teach program analysis based on graph abstractions. If successful, the project will significantly enhance our ability to reason about software, which is vital for the software reliability upon which our society depends. Furthermore, the integrated research and education activities will facilitate the construction of 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.