Call for Papers

This is for your information only. The workshop has occurred.


                       Call for Papers
                     Post-CAV Workshop on
                     Runtime Verification

                        23 July, 2001
                        Paris, France

        The workshop will be arranged as one of five approved
     satellite workshops on the final day of the CAV conference:


The objective of RV'01 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 whether the use of lightweight formal methods 
applied during the execution of programs is a viable complement 
to the current heavyweight methods proving programs correct always 
before their execution, such as model checking and theorem proving. 
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 

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.

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 

Both foundational and practical aspects or dynamic monitoring are 


Submissions should be extended abstracts of 8-12 pages, describing
recent  work,  work-in-progress, and even highly speculative work  on all
aspects of dynamic program monitoring and analysis.

Topics of interest include, but are not limited to, the  following:

- Specification languages and logics for program monitoring.
- Tools for analyzing (at runtime) the coherence between design patterns
  and code.
- Dynamic program analysis techniques.
- Tools for tracing and dynamic analysis of concurrent/distributed systems.
- Multi-threading analysis, such as deadlock and data race detection.
- Detection of significant events in concurrent/distributed computations.
- Event extraction: how to instrument source code or object code
  to emit events during execution to an observer.
- Program execution guidance to expose errors, for example randomness.
- Dynamic testing techniques based on dynamic feed-back.
- Program correction on-the-fly, based on violation of a specification
  during program execution.

Submissions should be sent to one of the organizers.

Accepted abstracts should be extended to at least 10 pages in order to
be published in Electronic Notes in Theoretical Computer Science:

together with papers from four other Post-CAV workshops.


  Submissions:   May  25, 2001
  Notification:  June 10, 2001
  Final papers:  June 30, 2001
  Workshop:      July 23, 2001



  Saddek Bensalem   (VERIMAG, France)
  Rance Cleaveland  (State University of New York at Stony Brook, USA)
  Michael Ernst     (Massachusetts Institute of Technology, USA)
  Patrice Godefroid (Bell Laboratories, USA)
  Gerard Holzmann   (Bell Laboratories, USA)
  Jim Larus         (Microsoft Research, USA)
  Insup Lee         (University of Pennsylvania, USA)
  John Rushby       (SRI International, USA)
  Joseph Sifakis    (VERIMAG, France)
  Reid Simmons      (Carnegie Mellon University, USA)
  Oleg Sokolsky     (University of Pennsylvania, USA)


  Klaus Havelund   (NASA Ames Research Center/Kestrel Technology, USA)
  Grigore Rosu     (NASA Ames Research center/RIACS, USA)


  The workshop will most likely be held at Jussieu University
  in the heart of Paris: