The RV series of workshops brings together researchers from academia and industry who are interested in runtime verification. The goal of the RV workshops is to study the ability to apply lightweight formal verification during the execution of programs. This approach complements the offline use of formal methods which often use large resources. Runtime verification methods and tools include the instrumentation of code with pieces of software that can help to test and monitor it online and detect, and sometimes prevent, potential faults.
RV 2009 was held on June 26-28 in Grenoble, France, adjacent to CAV 2009. The program included 11 accepted papers. Two invited talkswere given by Amir Pnueli on "Compositional Approach to Monitoring Linear Temporal Logic Properties" and Sriram Rajamani on "Verification, Testing and Statistics". The program also included three turorials.
Author(s): Howard Barringer, Klaus Havelund, David Rydeheard, Alex Groce (auth.), Saddek Bensalem, Doron A. Peled (eds.)
Series: Lecture Notes in Computer Science 5779 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2009
Language: English
Pages: 203
Tags: Software Engineering; Performance and Reliability; Programming Languages, Compilers, Interpreters; System Performance and Evaluation; Algorithm Analysis and Problem Complexity; Logics and Meanings of Programs
Front Matter....Pages -
Rule Systems for Runtime Verification: A Short Tutorial....Pages 1-24
Verification, Testing and Statistics....Pages 25-25
Type-Separated Bytecode – Its Construction and Evaluation....Pages 26-39
Runtime Verification of Safety-Progress Properties....Pages 40-59
Monitor Circuits for LTL with Bounded and Unbounded Future....Pages 60-75
State Joining and Splitting for the Symbolic Execution of Binaries....Pages 76-92
The LIME Interface Specification Language and Runtime Monitoring Tool....Pages 93-100
A Concurrency Testing Tool and Its Plug-Ins for Dynamic Analysis and Runtime Healing....Pages 101-114
Bridging the Gap between Algebraic Specification and Object-Oriented Generic Programming....Pages 115-131
Runtime Verification of C Memory Safety....Pages 132-151
A Combined On-Line/Off-Line Framework for Black-Box Fault Diagnosis....Pages 152-167
Hardware Supported Flexible Monitoring: Early Results....Pages 168-183
DMaC : Distributed Monitoring and Checking....Pages 184-201
Back Matter....Pages -
