Tools for automatic program analysis promise to improve programmer productivity by searching and summarizing large bodies of code. However, the phenomenon of aliasing --- different names being used to refer to the same data --- places fundamental limits on the effectiveness of simple textual analyses. My thesis system, Ajax, addresses this problem by incorporating static alias analysis into a number of different tools to aid Java programmers. The system handles arbitrary Java programs and has been evaluated against real Java applications such as the Javac Java compiler and the Javafig graphic editor.
In contrast to previous approaches, Ajax imposes a clean separation between analyis engines that produce alias information and tools that consume it. Analyses are treated as "black boxes" satisfying a simple, formal specification given in terms of the semantics of Java bytecode. Knowing only this specification, one can build many different tools with only a small amount of code. I have demonstrated the flexibility and efficiency of the design by building and evaluating tools for previously addressed problems such as finding dead code and resolving Java virtual method calls, and also by creating novel tools for statically checking Java downcasts, searching for accesses to objects, and building object models.
To support these tools, I have built a novel static analysis engine for Java called SEMI, based on type inference with polymorphic recursion. SEMI provides fully context-sensitive analysis of large programs. Using SEMI, Ajax can prove the safety of more than 50% of the downcast instructions in some real-life Java programs.
BIO: Robert O'Callahan recently completed his PhD degree at Carnegie Mellon. In addition to Ajax, he also built Lackwit, a similar system for analyzing C code, and spent some time at DEC SRC and IBM Watson working on dynamic program analysis tools. However, he is probably best known for creating the TTSSH free SSH client for Windows. Building, maintaining and supporting TTSSH over the years has given him some insight into the design of secure, user-proof software.
Robert obtained his Bachelor of Science degree from Auckland University, in New Zealand, which is the most beautiful country in the world.