RV Program is up

Eric | August 31, 2010

RV ConferenceThe program for RV 2010 is now available. (clap)

Comments Off on RV Program is up
Malta, RV

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 Off on Clara: a Framework for Partially Evaluating Finite-state Runtime Monitors Ahead of Time
Clara, Runtime Monitoring, Runtime verification, RV, RV 2010

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 Off on Save the Date: Nov 1st-4th – Clara Tutorial at RV 2010
Clara, Runtime verification, RV, Static Analysis

Submission deadline in 2 months: RV 2010 at Malta

Eric | March 30, 2010

RV Conference










Just in case you did not know yet: RV is becoming a conference. Submissions are due June 1st.

Runtime  verification (RV)  is concerned with monitoring and analysis of software  or hardware system executions.  The field is often referred to under different names, such as runtime verification, runtime monitoring, runtime  checking,   runtime  reflection,   runtime  analysis,   dynamic analysis,  symbolic dynamic analysis, trace analysis, log file analysis, etc.  RV can be used for many  purposes,  such as program understanding, systems  usage  understanding,  security  or  safety  policy monitoring,
debugging,  testing,  verification  and  validation,  fault  protection, behavior  modification (e.g.,  recovery),  etc.  A running system can be abstractly regarded as a generator of execution traces,  i.e., sequences of relevant  states or events.  Traces can be processed in various ways, e.g.,  checked  against formalized specifications, analyzed with special algorithms,  visualized,  etc.

Read the rest of this entry »

Comments Off on Submission deadline in 2 months: RV 2010 at Malta