Research Summary

The goal of my research is to create tools that support the development of complex software systems. The aim is to create tools that help programmers develop correct, reliable, efficient, and secure software by providing powerful operations for manipulating programs and analyzing their properties. The tools are based on understanding the meaning of the underlying programming language as well as some desired specified properties.

In particular, I am interested in automatic program verification. The main technique that I have been using is static analysis (also called abstract interpretation). This technique allows one to answer computationally hard questions about programs in an efficient albeit conservative way. I am interested in developing algorithms for general classes of static analysis problems and in efficiently solving particular instances of such problems. Most of our effort is focused on Shape Analysis.

I am interested in other aspects of static analysis including interprocedural analysis, reasoning tools, and program termination,

Interprocedural Analysis

In 1993-95, Susan Horwitz, Tom Reps, and myself developed efficient algorithms to perform interprocedural analysis. The algorithm was implemented in the SLAM tool for checking correctness of device drivers. The algorithm was implemented in several program analysis tools including SOOT and Wala. The algorithm was implemented in the codesurfer tool. In 2011 it was awarded an ACM SIGSOFT Retrospective Impact Paper Award.

Noam Rinetzky studied the problem of interprocedural analysis of programs manipulating dynamically allocated data structures. The problem is challenging since the program state is unbounded in two possible ways: (1) the program can allocate new elements and (2) procedure invocations allocates new memory for local variables. In his master thesis, Noam developed an algorithm for effectively summarizing dynamically allocated memory and activation records. In his Phd thesis Noam identified the concept of cutpoints which are objects which can be reached from the outside of a method without passing an object pointed by an actual parameter. He utilized cutpoints for better interprocedural analysis. He also developed a modular shape analysis algorithm that enforces dynamic encapsulation.

Bottom-Up (Compositional) Interprocedural Analysis

Scaling program analysis to large programs is an ongoing challenge for program verification. Typical programs include many relatively small procedures. Therefore, a promising direction for scalability is analyzing each procedure in isolation, using pre-computed summaries for called procedures and computing a summary for the analyzed procedure. Such analyses are called bottom-up interprocedural analysis or compositional analysis. Notice that the analysis of the procedure itself need not be compositional and can be costly.

Isil Dillig, Thomas Dillig, Alex Aiken and myself have shown how to perform precise bottom-up analysis for heap manipulating programs using constraints.

Ghila Castelnuovo, Mayur Naik, Noam Rinetzky, Hongseok Yang and myself have shown that when the analysis is specified using modular lattices then precise bottom-up interprodural analysis can be performed.

Program Analysis and Automatic Reasoning

An interesting question for program analysis and verification is how to automatically compute the effect of a program statement. This problem is especially interested for programs with unbounded and withy tricky changes.