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.

• In a paper by Tom Reps, Greta Yorsh, and myself it is shown how to utilize theorem provers to compute transformers for arbitrary abstractions. In a follow-up paper we show how to compute transformers for shape analysis using theorem provers.

  Program Termination

  I have also collaborated with Byron Cook on proving program termination.

  Past Research

  Buffer and String Analysis

  The goal of this research is to verify the absence of string manipulation errors such as accesses beyond buffer length in arbitrary C programs. This requires automatically inferring linear relationships between pointer expressions in the analyzed program.

  This research was conducted by Nurit Dor. Her thesis is available.

  Dynamic Analysis

  Our group also developed efficient algorithms for dynamically monitoring behavior while the program is executing. This information can be used by a compiler writer to estimate the potential improvement of suggested optimization. It can also be used by Just-In-Time compilers to dynamically apply a given optimization. Finally, it can also be used by a programmer to rewrite her code. We have collected different of information:

  • This research was done by David Oren and Boris Litvin, as part of their master studies under the supervision of Yossi Matias and myself.
  • Heap usage profiling. Our tools can locate opportunities for reducing the heap consumption of Java programs. This research was conducted by Michael Pan as part of his master thesis and Ran Shaham as part of his PhD thesis.
  • Recently, Percy Liang, , Mayur Naik, and myself conducted a dynamic analysis in order to determine the the Precision of Static Heap Abstractions