[aosd-announce] Call for Papers: Runtime Verification 2007 (with AOSD, Vancouver, BC)
Klaus Havelund
havelund at gmail.com
Sun Nov 26 22:36:23 EST 2006
Call for Papers
RV'07
Seventh Workshop on Runtime Verification
http://www.cis.upenn.edu/~rtg/rv2007/<http://www.cis.upenn.edu/%7Ertg/rv2007/>
March 13, 2007
Vancouver, BC, Canada
Affiliated with the 6th Intl. Conference on
Aspect-Oriented Software Development (AOSD'07)
http://aosd.net/2007/
RV'07 brings researchers together in order to debate how to monitor
and analyze the execution of programs. The focus of runtime
verification varies from testing software before deployment, detecting
errors after deployment and triggering fault protection mechanisms to
augmenting software with new capabilities in an aspect-oriented style.
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.
This year's workshop is organized as a satellite event of AOSD to
specifically create a synergy between the fields of runtime
verification and aspect-oriented programming. Within the recent few
years a trend has emerged in the aspect oriented community to extend
pointcut languages to richer trace predicate languages, including
regular expressions, state machines, temporal logic and grammars. This
trend obviously points to a future synergy between the two fields
since runtime verification studies exactly these kinds of problems.
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:
Techniques for guiding the behavior of a program once its
specification is violated. This ranges from standard exceptions to
advanced planning.
- 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,
can include program visualization.
Both foundational and practical aspects or dynamic monitoring are
encouraged.
SUBMISSIONS:
Authors are asked to submit a two-page abstract of their workshop
presentations which describe recent work, work-in-progress, and even
highly speculative work. The program committee will select the
presentations that will appear at the workshop.
After the workshop, the program committee will invite the presenters
to submit a full paper to be published in the post-workshop
proceedings. These submissions will be reviewed by the program
committee. We have applied for the post-proceedings to be published as
a Springer LNCS volume.
Information regarding the procedure for submissions will be available
on the workshop website
http://www.cis.upenn.edu/~rtg/rv2007/<http://www.cis.upenn.edu/%7Ertg/rv2007/>
DATES:
Submissions: January 15, 2007
Notification: January 29, 2007
Workshop: March 13, 2007
WEBSITE: http://www.cis.upenn.edu/~rtg/rv2007/<http://www.cis.upenn.edu/%7Ertg/rv2007/>
PROGRAM COMMITTEE:
Mehmet Aksit (University of Twente, NL)
Howard Barringer (University of Manchester, UK)
Saddek Bensalem (VERIMAG Laboratory, FR)
Eric Bodden (McGill Univeristy, CA)
Bernd Finkbeiner (Saarland University, DE)
Cormac Flanagan (University of California, Santa Cruz, US)
Vijay Garg (University of Texas, Austin, US)
Klaus Havelund (NASA Jet Propulsion Laboratory/Columbus
Technologies, US)
Gerard Holzmann (NASA Jet Propulsion Laboratory, US)
Moonzoo Kim (KAIST, KR)
Martin Leucker (Technical University of Munich, DE)
Oege de Moor (Oxford University, UK)
Klaus Ostermann (Darmstadt University of Technology, DE)
Shaz Qadeer (Microsoft Research, US)
Grigore Rosu (University of Illinois, Urbana-Champaign, US)
Henny Sipma (Stanford University, US)
Oleg Sokolsky (University of Pennsylvania, US)
Scott Stoller (State University of New York, Stony Brook, US)
Mario Sudholt (Ecole des Mines de Nantes-INRIA, LINA, FR)
Serdar Tasiran (Koc University, TR)
ORGANIZING COMMITTEE:
Oleg Sokolsky (University of Pennsylvania)
Serdar Tasiran (Koc University)
STEERING COMMITTEE:
Klaus Havelund (NASA Jet Propulsion Laboratory/Columbus Technologies)
Gerard Holzmann (NASA Jet Propulsion Laboratory)
Insup Lee (University of Pennsylvania)
Grigore Rosu (University of Illinois, Urbana-Champaign)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: /pipermail/announce_aosd.net/attachments/20061126/8ef39d26/attachment.html
More information about the announce
mailing list