Runtime Verification and Monitoring

[Grigore Rosu <grosu AT cs.uiuc.edu>]

RV (http://mail.cs.uiuc.edu/mailman/listinfo/rv) is a moderated discussion
forum for scientists interested in all aspects of verification, analysis
and monitoring of systems at runtime.  If you want to post a message on
this list just send it to 
rv AT cs.uiuc.edu
 and, if appropriate, will be
posted by the moderator 
(grosu AT cs.uiuc.edu).

The reason for which you receive this message is because we think that you
would like to join this list.  If you would NOT like to be on this list,
please reply to this message and let us know that; we will remove your
address from the list immediately.  If you believe that other scientists,
including your students, would like to also be on the list, we would be
more than happy to add them.  Just send us their email addresses.  They
can also subscribe themselves at http://mail.cs.uiuc.edu/mailman/listinfo/rv.
At the end of this message there is a list of all the current addresses on
the rv list, sorted alphabetically.

Appended is also a Call for Papers for the RV'04 workshop that will be
held in Barcelona as a satelite event to ETAPS'04.  The description of the
workshop below contains also the desired topics of interest for the RV
list.  We will make any possible effort to keep the number of messages
low and definitely will allow no spam on this list.

Grigore Rosu
Klaus Havelund

-----------------------------------------------------------------------

                       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)

----------------------------------------------------------------------
Addresses on the RV list

agates AT cs.utep.edu
am AT cl.cam.ac.uk
amir AT cs.nyu.edu
amir AT wisdom.weizmann.ac.il
bkarthik AT seas.upenn.edu
Celemens.Fischer AT ewe.de
cormac AT gtcse.ucsc.edu
crane AT cs.queensu.ca
Detlef.Bartetzko AT atanicon.com
dingel AT cs.queensu.ca
Doron.Peled AT dcs.warwick.ac.uk
ducasse AT irisa.fr
fengchen AT cs.uiuc.edu
finkbeiner AT cs.uni-sb.de
garg AT ece.utexas.edu
Gerard.J.Holzmann AT jpl.nasa.gov
god AT bell-labs.com
goldberg AT cs.nyu.edu
grosu AT cs.uiuc.edu
gunter AT cis.upenn.edu
gurevich AT microsoft.com
havelund AT email.arc.nasa.gov
Heike.Wehrheim AT informatik.uni-oldenburg.de
horwitz AT cs.wisc.edu
howard AT cs.man.ac.uk
jahier AT irisa.fr
Joseph.Sifakis AT imag.fr
jwnimmer AT lcs.mit.edu
kannan AT cis.upenn.edu
kgl AT cs.auc.dk
korten AT traclabs.com
ksen AT cs.uiuc.edu
larus AT microsoft.com
lee AT cis.upenn.edu
levy AT sdl.sri.com
liqiang AT cs.sunysb.edu
Mark.Broerkens AT offis.de
M.C.W.Geilen AT tue.nl
mernst AT lcs.mit.edu
Michael.Moeller AT informatik.uni-oldenburg.de
monjoo AT secui.com
muratk AT ti.com
ndelgado AT cs.utep.edu
nikolaj AT cs.stanford.edu
njn25 AT cam.ac.uk
oscar AT cs.utep.edu
parkera AT cs.ucsb.edu
phs AT lsv.ens-cachan.fr
rance AT cs.sunysb.edu
reids AT cs.cmu.edu
reids+ AT cs.cmu.edu
rpvenkat AT cs.uiuc.edu
Rushby AT csl.sri.com
Saddek.Bensalem AT imag.fr
saidi AT sdl.sri.com
sen AT ece.utexas.edu
Sergio.Yovine AT imag.fr
sipma AT cs.stanford.edu
sokolsky AT cis.upenn.edu
sroach AT cs.utep.edu
Stavros.Tripakis AT imag.fr
stoller AT cs.sunysb.edu
suan AT cs.wisc.edu
uribe AT sdl.sri.com
usa AT cis.upenn.edu
vmahesh AT cs.uiuc.edu
yifang AT cs.nyu.edu
zuck AT cs.nyu.edu