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. The tools are fully automatic and can operate on the program source files.

In particular, I am interested in automatic program verification. The main technique that I use 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 two topics:

• Shape Analysis
• String Analysis

Shape and Pointer Analysis

• There is no a-priori bound on the size of the concrete memory state,
• The control and the data of the program interact in a non-trivial manner.
• The program state can be changed in indirect ways using pointers and destructive-updates.

As part of this research we have developed TVLA, which was used to prove interesting properties of programs manipulating unbounded data structures including:

• Shape analysis of programs manipulating singly- and doubly-linked lists, and trees including interprocedural analysis .
• Proving correctness of implementations of sorting algorithms
• Proving safety and liveness properties in programs manipulating an unbounded number of objects and threads. This research was conducted by Eran Yahav

In the future, I plan to extend the work on heap analysis in several directions:

• Proving interesting safety properties of data structure implementations. For example, we have been using TVLA to verify the partial correctness of garbage collection implementations.
• Employing machine learning techniques in order to make the system more automatic. This research is conducted by Alexy Loginov
• Combining shape analysis and other abstract domains in order to handle programs with interactions between references and other data types. This research is conducted by Denis Gopan
• Using assume-guarantee reasoning to verify larger programs. This work will assume that the user specifies contracts describing the interfaces. This research is conducted by Greta Yorsh
• Verifying heap manipulation properties of object oriented programs. Here, we expect to develop notions of "encapsulation" for heap manipulating programs which allow flexible data structures implementation and reasoning. This research is conducted by Noam Rinetzky
• Developing efficient static analysis algorithms in TVLA to allow the verification of larger programs. The challenge here is to develop polynomial-time algorithms that can in many cases achieve the same precision of TVLA. This research is conducted by Roman Manevich

One of the challenging aspects of abstract interpretation is calculating the effect of programming language statements for parametric abstractions and for library calls. In order to compute the effect of such statements, we are developing theorem provers for linked data structures.

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. Ron Elebogen, Nurit, and Roberto Bagnara recently developed and implemented an interprocedural analysis of C programs that infers such linear relationships between pointer expressions in a fully automatic way. This work is part of Ron's master thesis

Profiling Tools

We also conducted research in order to develop 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 focused on two kinds of information:

• Subpath profiling in order to monitor the execution frequency of control flow subpaths. 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.