Runtime Verification and Monitoring

[Bernd Finkbeiner <finkbeiner AT cs.uni-sb.de>]

                   Call for Papers

                        RV'05

         Fifth Workshop on Runtime Verification
           http://react.cs.uni-sb.de/rv2005/

                    July 12, 2005  

        The University of Edinburgh, Scotland, UK 
 
               Affiliated with CAV'05
          http://www.cav2005.inf.ed.ac.uk/

The objective of RV'05 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:

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.

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. 

Information regarding the procedure for submissions will be available
on the workshop website http://react.cs.uni-sb.de/rv2005/

DATES:

Submissions:  April 9, 2005 
Notification:  May 14, 2005
Final papers:  June 11, 2005
Workshop:  July 12, 2005

WEBSITE:

http://react.cs.uni-sb.de/rv2005/

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:

Howard Barringer  (The University of Manchester)
Bernd Finkbeiner  (Universitaet des Saarlandes)
Yuri Gurevich  (Microsoft Research)
Henny Sipma  (Stanford University)