Runtime Verification and Monitoring

["Klaus Havelund" <havelund AT gmail.com>]

          Second Call for Papers
                      RV'07

 *** Extended submission deadline: January 26, 2007 ***

        Seventh Workshop on Runtime Verification
         

http://www.cis.upenn.edu/~rtg/rv2007/
                   March 13, 2007
                Vancouver, BC, Canada
       Affiliated with the 6th Intl. Conference on
      Aspect-Oriented Software Development (AOSD'07)
                 http://aosd.net/2007/

RV'07
brings researchers together in order to debate how to monitor and
analyze the execution of programs. The focus of runtime verification
varies from testing software before deployment, detecting errors after
deployment and triggering fault protection mechanisms to augmenting
software with new capabilities in an aspect-oriented style.
Approaches
to runtime verification include checking conformance with a formal
specification written in a temporal or history-tracking logic. One of
the longer-term goals of the workshop is to investigate the use of
lightweight formal methods applied at runtime as a viable complement to
methods aimed mainly at proving programs correct prior to execution,
e.g., theorem proving and model checking.

This year's workshop
is organized as a satellite event of AOSD to specifically create a
synergy between the fields of runtime verification and aspect-oriented
programming. Within the recent few years a trend has emerged in the
aspect oriented community to extend pointcut languages to richer trace
predicate languages, including regular expressions, state machines,
temporal logic and grammars. This trend obviously points to a future
synergy between the two fields since runtime verification studies
exactly these kinds of problems.

The subject covers several technical fields as outlined below.

- Specification languages and logics:
Formal
methods scientists have investigated logics and developed technologies
that are suitable for model checking and theorem proving, but
monitoring can reveal new observation-based foundational logics.

- Aspect oriented languages with trace predicates:
New results in extending aspect languages, such as for example AspectJ, with trace predicates replacing the standard pointcuts.
Aspect oriented programming provides specific solutions to program instrumentation and program guidance.

- Program instrumentation in general:
Any
techniques for instrumenting programs, at the source code or object
code/byte code level, to emit relevant events to an observer.

- Program Guidance in general:
Techniques
for guiding the behavior of a program once its specification is
violated. This ranges from standard exceptions to advanced planning.

- Combining static and dynamic analysis:
Monitoring
a program with respect to a temporal formula can have an impact on the
monitored program, with respect to execution time as well as memory
consumption. Static analysis can be used to minimize the impact by
optimizing the program instrumentation. Runtime monitors can be seen as
proof obligations left over from proofs - what is left that could not
be proved.

- Dynamic program analysis:
Techniques that gather
information during program execution and use it to conclude properties
about the program, either during test or in operation. Algorithms for
detecting multi-threading errors in execution traces, such as deadlocks
and data races. Algorithms for generating specifications from runs --
dynamic reverse engineering, can include program visualization.

Both foundational and practical aspects or dynamic monitoring are encouraged.

SUBMISSIONS:

Authors
are asked to submit a two-page abstract of their workshop presentations
which describe recent work, work-in-progress, and even highly
speculative work. The program committee will select the presentations
that will appear at the workshop.

After the workshop, the
program committee will invite the presenters to submit a full paper to
be published in the post-workshop proceedings.  These submissions will
be reviewed by the program committee. We have applied for the
post-proceedings to be published as a Springer LNCS volume.

Information regarding the procedure for submissions will be available on the workshop website 

http://www.cis.upenn.edu/~rtg/rv2007/

DATES:

Submissions:  January 26, 2007 (Extended)
Notification: February 2, 2007
Workshop:     March 13, 2007

WEBSITE:      

http://www.cis.upenn.edu/~rtg/rv2007/

PROGRAM COMMITTEE:

Mehmet Aksit          (University of Twente, NL)
Howard Barringer      (University of Manchester, UK)
Saddek Bensalem       (VERIMAG Laboratory, FR)
Eric Bodden           (McGill Univeristy, CA)
Bernd Finkbeiner      (Saarland University, DE)
Cormac Flanagan       (University of California, Santa Cruz, US)
Vijay Garg            (University of Texas, Austin, US)
Klaus Havelund        (NASA Jet Propulsion Laboratory/Columbus
Technologies, US)
Gerard Holzmann       (NASA Jet Propulsion Laboratory, US)
Moonzoo Kim           (KAIST, KR)
Martin Leucker        (Technical University of Munich, DE)
Oege de Moor          (Oxford University, UK)
Klaus Ostermann       (Darmstadt University of Technology, DE)
Shaz Qadeer           (Microsoft Research, US)
Grigore Rosu          (University of Illinois, Urbana-Champaign, US)
Henny Sipma           (Stanford University, US)
Oleg Sokolsky         (University of Pennsylvania, US)
Scott Stoller         (State University of New York, Stony Brook, US)
Mario Sudholt         (Ecole des Mines de Nantes-INRIA, LINA, FR)
Serdar Tasiran        (Koc University, TR)

ORGANIZING COMMITTEE:

Oleg Sokolsky  (University of Pennsylvania)
Serdar Tasiran (Koc University)

STEERING COMMITTEE:

Klaus Havelund   (NASA Jet Propulsion Laboratory/Columbus Technologies)
Gerard Holzmann  (NASA Jet Propulsion Laboratory)
Insup Lee        (University of Pennsylvania)
Grigore Rosu     (University of Illinois, Urbana-Champaign)