Patrick Lam

Associate Professor, Department of Electrical and Computer Engineering
Director, Software Engineering Programme
University of Waterloo
email: patrick.lam@uwaterloo.ca (no unsolicited commercial email)
phone: use email instead!

Picture of Patrick Lam

Static Analysis of Tracematches

Tracematches enable the specification of program properties that relate the states of multiple objects. They are especially useful for specifying library usage constraints: for instance,

We believe that tracematches are useful for checking many safety properties of Java programs, since many Java programs are structured as a collection of libraries with some driver code.

Structure of Tracematches

Developers specify tracematches using an extension to AspectJ. We can understand tracematches by representing them with finite automata, like the one below:

hasNext automaton

A tracematch declaration contains (1) tracematch variables; (2) event declarations; (3) a regular expression over the declared events; and (4) code to execute if the program's execution matches the regular expression. We can write the above tracematch as follows:

tracematch(Iterator i) {
    sym hasNext before: call(* java.util.Iterator+.hasNext()) && target(i);
    sym next before: call(* java.util.Iterator+.next()) && target(i);

    next next {
        /* handle error */
    }

Research Goal

The goal of our research on tracematches is to statically analyze tracematches and determine when they cannot trigger. For tracematches that describe software safety properties, if we can statically verify that a tracematch never triggers, then we have statically verified the desired safety property.

With Eric Bodden and Laurie Hendren, I have therefore worked on the static analysis of tracematches.

Valid HTML 5!