Call for Papers

RV'07

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 Softare 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
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)