CFP: RV'08
Martin Leucker
rv08 at in.tum.de
So Sep 16 01:20:20 CEST 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 has been extended 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) (to be confirmed).
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:
Abstracts: December 9, 2007
Submissions: December 14, 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)
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)
Mehr Informationen über die Mailingliste IFI-CI-Event