Runtime Verification and Monitoring

[Martin Leucker <leucker AT in.tum.de>]

=====================================================================
Due to numerous requests:

Submission Deadline now: December 21st, 2007

=====================================================================

We apologize if you receive multiple copies of this email.

----------------------------------------------------------------------
                           Call for Papers

                                RV'08
                 8th Workshop on Runtime Verification

                        http://rv08.in.tum.de/
                            March 30, 2008
                          Budapest, Hungary

                       Affiliated with ETAPS'08
                      http://etaps08.mit.bme.hu/
----------------------------------------------------------------------

RV'08  brings together researchers in  order  to debate how to monitor
and  analyze  the  execution   of   programs. The  focus   of  runtime
verification varies    from  testing  software before   deployment  to
detecting errors after deployment.  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.

Moreover, the  focus of RV  ranges from detecting (non)-conformance to
triggering  fault protection  mechanisms  in case non-conformance  has
been detected.  This  allows for  new software design  and programming
paradigms.  Thus,  RV's topics partially overlap   with those found in
other directions such   as aspect oriented  programming,  self-healing
systems, autonomous systems, adaptive systems, etc.

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:

      Methodologies, architectures,  and  techniques  for  guiding the
      behavior  of a program  once  its specification is violated, for
      developing    self-healing,     autonomous,    or       adaptive
      systems. Techniques ranging from standard exceptions to advanced
      planning  lead  to  new development  methodologies  and software
      architectures  such    as    monitor-oriented    programming  or
      monitor-based runtime reflection.

    * 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, including     also    program
      visualization.

    * Security analysis:

      Monitoring for the enforcement  of security policies. Successful
      applications  include   operating system and   middleware access
      control, firewalls, stack inspection based sandboxing, detecting
      the    threats of untrustworthy     (malicious or  buggy)  code,
      intrusion detection etc.

    * Contract Security analysis:

      Monitoring for the enforcement   of contract fulfillment in  SOA
      and  web-services,    especially  in contract-oriented  software
      development.

Both foundational and practical aspects are encouraged.

PROCEEDINGS:

Preliminary workshop proceedings will be available at the meeting as a
technical report.   As for RV'07, revised  final papers will appear as
Springer Lecture Notes in Computer Science (LNCS).

SUBMISSIONS:

    * All submissions should  be made electronically on the Submission
      Page.

    * Manuscripts of regular  papers are  limited to  a maximum of  15
      pages (excluding technical appendices) in PDF format (LNCS style
      mandatory).

DATES:

Submissions:            December 21, 2007
Notification:           January 14, 2008
Camera ready copy:      January 28, 2008
Workshop:               March 30, 2008

INVITED SPEAKER:

Jean Goubault-Larrecq:  Orchids, and Bad Weeds

PROGRAM COMMITTEE:

Mehmet Aksit            (University of Twente, NL)
Howard Barringer        (University of Manchester, UK)
Mads Dam                (KTH Stockholm, SE)
Bernd Finkbeiner        (Saarland University, DE)
Klaus Havelund          (NASA Jet Propulsion Laboratory, US)
Bengt Jonsson           (Uppsala Univesitet, SE)
Moonzoo Kim             (KAIST, KR)
Martin Leucker (Chair)  (Technical University of Munich, DE)
Dejan Nickovic          (Verimag, FR)
Doron Peled             (Bar Ilan University, IL)
Mauro Pezze             (University of Lugano, CH)
Shaz Qadeer             (Microsoft Research, US)
Grigore Rosu            (University of Illinois, Urbana-Champaign, US)
Gerardo Schneider       (University of Oslo, NO)
Henny Sipma             (Stanford University, US)
Oleg Sokolsky           (University of Pennsylvania, US)
Scott Stoller           (State University of New York, US)
Mario Sudholt           (Ecole des Mines de Nantes-INRIA, LINA, FR)
Serdar Tasiran          (Koc University, TR)
Stavros Tripakis        (Cadence Labs, US)
Yaron Wolfsthal         (IBM, IL)

STEERING COMMITTEE:

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