EECS Joint Colloquium Distinguished Lecture Series

Wednesday, September 29, 2004
Hewlett Packard Auditorium, 306 Soda Hall
4:00-5:00 p.m.

Dr. Shmuel Sagiv

School of Computer Science
Tel-Aviv University


Compile-Time Verification of Properties of Heap Intensive Programs




Existing programs contain runtime errors such as buffer overruns, dangling dereferences and memory leaks. They cause unpredictable behaviors, system crashes and are exploited by hackers to break existing systems.

This work is part of an attempt to catch these runtime errors at compile-time. Our methods are sound (conservative), i.e., whenever the compiler issues no warnings, we can guarantee that no runtime error will ever occur. However, our methods can issue "false alarms", i.e., warnings against potential runtime errors that can never occur. This is in line with the undecidability of checking these properties.

Specifically, we develop methods for summarizing dynamically allocated storage and pointers by only tracking the "shape" of the heap and use these summarizations for proving the absence of runtime errors.

These methods can automatically prove properties ranging from the absence of null dereferences and memory leaks to partial and total correctness. The algorithms were implemented and applied to C and Java programs. Our current algorithms have very few false alarms but are rather expensive. I will also sketch several methods that may be used to scale this method to larger programs.

This is a joint work with Thomas Reps from the University of Wisconsin and Reinhard Wilhelm from the Saarland University:


Dr. Sagiv received his Ph.D. in Computer Science from Technion Israel Institute of Technology, Haifa. He joined Tel Aviv University's School of Computer Science in 1997 and has been a Senior Lecturer there since 2000. He has been a visiting professor at the University of Chicago and Datalogisk Institute at the University of Copenhagen. In addition, he has been a researcher at the University of Wisconsin-Madison and IBM's Israel Scientific Center. His research interests include Programming Languages, Compilers, Abstract interpretation, Profiling, Pointer Analysis, Shape Analysis, Interprocedural dataflow analysis, Program Slicing, and Language-based programming environments.