Eric Bodden

11°C

In my publications section you can now find our RV 2010 paper on the Clara Framework. This is by far the most concise introduction to Clara; therefore I hope that people will find it more accessible than my thesis. download the paper here

Abstract: Researchers have developed a number of runtime verification tools that generate runtime monitors in the form of AspectJ aspects. In this work, we present Clara, a novel framework to statically optimize such monitoring aspects with respect to a given program under test. Clara uses a sequence of increasingly precise static analyses to automatically convert a monitoring aspect into a residual runtime monitor. The residual monitor only watches events triggered by program locations that the analyses failed to prove safe at compile time. In two-thirds of the cases in our experiments, the static analysis succeeds on all locations, proving that the program fulfills the stated properties, and completely obviating the need for runtime monitoring. In the remaining cases, the residual runtime monitor is usually much more efficient than a full monitor, yet still captures all property violations at runtime.

Dear all, for all of those of you who happened to be in Chile in November: I will be giving a lecture about the latest techniques in analyzing Java programs with Soot at the 3rd Summer School on Programming Languages, which is co-located with the Chilean Computing Week. You can find more information here. At the same even, I will moreover be giving a hands-on tutorial on Clara (“Partially evaluating finite-state runtime monitors ahead-of-time”), which is likely going to be similar to my RV tutorial.

Joint work with Chang Hwan Peter Kim, Don Batory, and Sarfraz Khurshid, to appear at RV 2010.

Abstract: A software product line is a family of programs where each program is defined by a unique combination of features. Product lines, like conventional programs, can be checked for safety properties through execution monitoring. However, because a product line induces a number of programs that is potentially exponential in the number of features, it would be very expensive to use existing monitoring techniques: one would have to apply those techniques to every single program. Doing so would also be wasteful because many programs can provably never violate the stated property. We introduce a monitoring technique dedicated to product lines that, given a safety property, statically determines the feature combinations that cannot possibly violate the property, thus reducing the number of programs to monitor. Experiments show that our technique is effective, particularly for safety properties that crosscut many optional features.

Download the paper here.

Today I am having good news for everybody who is working on runtime monitoring in a Java-based setting and is thinking about using my Clara framework for partially evaluating runtime monitors at compile time. My tutorial proposal for RV 2010 has just been accepted.

For now, I am planning to cover the following topics:

• Problem Statement: Why partial evaluation?
• What’s out there? Overview of existing runtime-monitoring tools
• Architecture of Clara: Important Design Decisions
• Static analyses in Clara: How do they work? How can we use them?
  • Quick Check: syntactic, flow-insensitive
  • Orphan-Shadows Analysis: pointer-based, flow-insensitive
  • Nop-Shadows Analysis: pointer-based, flow-sensitive
• Clara as a generic optimizer: How to allow your own runtime-verification tool to use Clara for static optimizations

If time permits also:

• Clara and testing: Using Clara to tell apart useful from useless test cases

You can read the full tutorial proposal here. Patrick Lam will likely be joining me for the fun. We will likely be allocated a 2.5h slot, which is not a lot of time to cover all these topics. Therefore, if you would like me to cover some special topic in more detail than others, don’t be shy and let me know

P.S. Also don’t forget that the paper submission deadline for RV is approaching quickly: June 1st!

Several people asked me for the slides of my ICSE presentation. I have just uploaded them, as Keynote and PDF (quite large). Enjoy!

P.S. Thanks to Zhifeng Lai for taking the picture!

I am happy to announce that the camera-ready version of my ICSE paper is available now. The topic is on a special kind of static typestate analysis that I developed to soundly disable unnecessary instrumentation for monitoring typestate properties at runtime. The implementation is available in Clara.

On November 11th I passed my thesis defense in Montreal. Thanks a lot to everybody who congratulated me already! The event was fun, actually. I received many questions by my committee but fortunately I was able to answer all of them.

Here are two photos of the event.

Lots of people commented on my slides and so I thought that I should put them online. Here is an extended version of the talk, which I presented in Darmstadt. Available for Keynote (25 MB) and as PDF (93 MB – yes I do like using lots of pictures). The slides give information about both the Clara framework and the Nop-Shadows Analysis.