Runtime Verification and Monitoring

[havelund AT email.arc.nasa.gov]

                    Final Call for Papers

                            RV'04
           Fourth Workshop on Runtime Verification
                http://ase.arc.nasa.gov/rv2004

                       April 3-4, 2004  

                       Barcelona, Spain
 
                   Affiliated with ETAPS'04
                 http://www.lsi.upc.es/etaps04



OBJECTIVE

The objective of RV'04 is to bring scientists from both academia 
and industry together to debate on how to monitor, analyze and 
guide the execution of programs.  The ultimate longer term goal 
is to investigate the use of lightweight formal methods applied 
during the execution of programs from the following two points of
view.  On the one hand, whether run-time application of formal methods 
is a viable complement to the traditional methods proving 
programs correct before their execution, such as model checking 
and theorem proving.  On the other hand, whether formality
improves traditional ad-hoc monitoring techniques used in 
performance monitoring, distributed debugging, etc.  Dynamic program 
monitoring and analysis can occur during testing or during operation. 
The subject covers several technical fields as outlined below.

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.

Specification Languages and Logics:
While scientists have investigated logics and developed technologies
that are suitable for model checking and theorem proving,
monitoring can reveal new observation-based foundational logics.

Program Instrumentation:
Techniques for instrumenting programs, at the source code or object
code/byte code level, to emit relevant events to an observer.

Program Guidance:
Techniques for guiding the behavior of a program once its specification
is violated. This ranges from standard exceptions to advanced planning.
Guidance can also be used during testing to expose errors.

Novel applications for run-time verification:
Formalisms that go beyond correctness properties.  This includes, but
certainly is not limited to, performance properties, survivability and
fault tolerance, and so on.

Both foundational and practical aspects of dynamic monitoring are 
encouraged.


SUBMISSIONS

The full submissions should be sent by **December 15, 2003**.
The accepted papers are expected to be published in Electronic Notes
in Theoretical Computer Science (ENTCS), and selected papers will be
considered for publication in a prestigious journal. 

Submissions should be up to 15 pages using the ENTCS format 
(http://math.tulane.edu/~entcs/) and should
describe recent work, work-in-progress, and even highly speculative
work on all aspects of dynamic program monitoring and analysis.

Abstracts and submissions should be sent to one or both of the organizers.

DATES:

  Submissions:    December 15, 2003
  Notification:   January 15, 2004
  Final papers:   February 15, 2004
  Workshop:       April 3-4, 2004

WEBSITE:

  http://ase.arc.nasa.gov/rv2004

PROGRAM COMMITTEE:

  Howard Barringer      (University of Manchester)
  Bernd Finkbeiner      (Saarland University)
  Cormac Flanagan       (University of California, Santa Cruz)
  Vijay Garg            (University of Texas, Austin)
  Ann Gates             (University of Texas, El Paso)
  Patrice Godefroid     (Bell Laboratories)
  Yuri Gurevich         (Microsoft Research)
  Kim Guldstrand Larsen (Aalborg University) 
  Jim Larus             (Microsoft Research)
  Doron Peled           (University of Warwick)
  Amir Pnueli           (The Weizmann Institute of Science)
  Henny Sipma           (Stanford University)
  Oleg Sokolsky         (University of Pennsylvania)
  Scott Stoller         (State University of New York, Stony Brook)
  Mahesh Viswanathan    (University of Illinois, Urbana-Champaign)
  Sergio Yovine         (VERIMAG Laboratory)
  Lenore Zuck           (New York University)

STEERING COMMITTEE:

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

ORGANIZING COMMITTEE:

  Klaus Havelund        (NASA Ames Research Center - Kestrel Technology) 
  Grigore Rosu          (University of Illinois, Urbana-Champaign)