RV'05 - Fifth Workshop on
Runtime Verification

Satellite workshop of CAV 2005.

July 12, 2005
The University of Edinburgh, Scotland, UK

Workshop Programme - Accepted Papers

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 runtime 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. There is an obvious relationship between runtime verification and aspect oriented programming.

Novel Applications for Runtime Verification. Formalisms that go beyond correctness properties. This includes, but certainly is not limited to, performance properties, survivability and fault tolerance, program visualization, and so on.

Both foundational and practical aspects of monitoring are encouraged.

RV'05 is sponsored by Microsoft Research.

Microsoft is a registered trademark of Microsoft Corporation.

Previous workshops:

RV'01 - First Workshop on Runtime Verification, Paris, July 2001

RV'02 - Second Workshop on Runtime Verification, Copenhagen, July 2002

RV'03 - Third Workshop on Runtime Verification, Boulder, July 2003

RV'04 - Fourth Workshop on Runtime Verification, Barcelona, April 2004