Statically Verifying Software Safety Properties with Tracematches

Tracematches enable developers to declaratively specify safety properties for Java programs. These properties can be either domain-specific properties (e.g. compiler passes are always executed in the correct order) or generic properties (e.g. linked lists are never modified during iteration). While it is possible to dynamically monitor tracematches, such an approach 1) carries runtime overhead and 2) does not suggest reasonable recovery actions. We investigate a static analysis that promises to reduce runtime overhead and, in some cases, can guarantee that a program will never violate certain safety properties (eliminating the need for recovery actions). Our approach propagates tracematch states through methods to ensure that unsafe states are never triggered during an execution, thereby enabling the elimination of runtime checks. Pointer analysis turns out to be important in the static analysis of tracematches, and I will discuss the various analyses needed to make our overall static analysis work.

This is joint work with Eric Bodden and Laurie Hendren.
Patrick Lam is an NSERC Postdoctoral Fellow at McGill University. He recently completed his PhD at the Massachusetts Institute of Technology, and will be joining the Electrical and Computer Engineering Department of the University of Waterloo in January 2008 as an Assistant Professor. His research interests focus on the application of static analysis techniques to software engineering problems.