Main

About me

Research

  (publications)

Teaching

Software

Random anecdote

Gallery

Judo Club

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,

• an Iterator's next method should not be called twice without any intervening call to hasNext;
• an Iterator's methods may not be called if the underlying Collection has been modified after Iterator creation; and
• in the Weka mechine learning toolkit, a Filter's setInputFormat method must be the last call before applying the Filter.

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:

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.

• Eric Bodden, Laurie Hendren, and Ondrej Lhotak. ECOOP 2007: A staged static program analysis to improve the performance of runtime monitoring. [bib] (I didn't write this paper, but I've included it as it provides context for the following papers.)
• Eric Bodden, Laurie Hendren, Patrick Lam, Ondrej Lhotak, Nomair A. Naeem. RV 2007: Collaborative runtime verification with tracematches [pdf, bib]. (Extended version under review for Journal of Logic and Computation.)
• Eric Bodden, Patrick Lam and Laurie Hendren. In proceedings of FSE 2008: Finding Programming Errors Earlier by Evaluating Runtime Monitors Ahead-of-Time.
• Eric Bodden, Patrick Lam and Laurie Hendren. In proceedings of Visions of Computer Science 2008, British Computer Society: Object Representatives: a uniform abstraction for pointer information.