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
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)
Scott Stoller (State University of New York, 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)