Clara: a Framework for Partially Evaluating Finite-state Runtime Monitors Ahead of Time

Eric | August 19, 2010

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.

Comments
Comments Off on Clara: a Framework for Partially Evaluating Finite-state Runtime Monitors Ahead of Time
Categories
Research
Tags
Clara, Runtime Monitoring, Runtime verification, RV, RV 2010

Lecture on Soot, Hands-on Tutorials on Clara

Eric | August 12, 2010

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.

Comments
Comments Off on Lecture on Soot, Hands-on Tutorials on Clara
Categories
Research
Tags
Chile, Clara, SCCC, Soot

Reducing Configurations to Monitor in a Software Product Line

Eric | July 26, 2010

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.

Comments
Comments Off on Reducing Configurations to Monitor in a Software Product Line
Categories
Research
Tags
Clara, Product Lines, Runtime verification

Save the Date: Nov 1st-4th – Clara Tutorial at RV 2010

Eric | May 18, 2010

RV ConferenceToday 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!

Comments
Comments Off on Save the Date: Nov 1st-4th – Clara Tutorial at RV 2010
Categories
Research
Tags
Clara, Runtime verification, RV, Static Analysis

ICSE Presentation slides now online

Eric | May 8, 2010

ICSE 2010 PresentationSeveral 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!

Comments
Comments Off on ICSE Presentation slides now online
Categories
Research
Tags
Clara, ICSE

New ICSE paper: Efficient Hybrid Typestate Analysis by Determining Continuation-Equivalent States

Eric | January 21, 2010

Screen shot 2010-01-21 at 13.46.04 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.

Comments
Comments Off on New ICSE paper: Efficient Hybrid Typestate Analysis by Determining Continuation-Equivalent States
Categories
Research
Tags
Clara, ICSE, Typestate

Slides and photos of defense talk

Eric | November 17, 2009

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.

IMG_0261

IMG_0258

 

 

 

 

 

 

 

Nop-shadows analysis in actionLots 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.

Comments
Comments Off on Slides and photos of defense talk
Categories
Research
Tags
Clara, Defense, Nop-shadows Analysis, Slides

New Tech Report: Efficient and Precise Typestate Analysis by Determining Continuation-Equivalent States

Eric | September 10, 2009

image

I just uploaded a new Technical Report. The report (currently under submission) describes a novel typestate analysis, called Nop-Shadows Analysis,  that I implemented for my doctoral dissertation. The analysis is certainly one of my dissertation’s major technical contributions. I implemented the Nop-Shadows Analysis in the Clara framework, which means that you are welcome to download it, try it out or extend it.

Read the rest of this entry »

Comments
Comments Off on New Tech Report: Efficient and Precise Typestate Analysis by Determining Continuation-Equivalent States
Categories
Research
Tags
Clara, Static Analysis, Typestate

Now available: Clara, a novel framework for implementing hybrid typestate analyses

Eric | September 10, 2009

ClaraIn my doctoral dissertation (click here for a draft), I present Clara (Compile-time Approximation of Runtime Analyses), a novel research framework for the implementation of hybrid typestate analyses. Clara is now online – fully documented – at: http://www.bodden.de/clara/

Typestate properties aid program understanding, and one can even define type systems that prevent programmers from causing typestate errors, or derive static typestate analyses that try to determine whether a given program violates typestate properties. Unfortunately, the typestate-analysis problem is generally undecidable. Researchers have therefore proposed a hybrid approach that uses
static-analysis results to generate a residual runtime monitor. This monitor captures actual property violations as they occur, but only updates its internal state at relevant statements, as determined through static analysis.

Read the rest of this entry »

Comments
Comments Off on Now available: Clara, a novel framework for implementing hybrid typestate analyses
Categories
Research
Tags
Clara, Runtime Monitoring, Runtime verification, Static Analysis, Thesis, tracematches, Typestate