22nd Intl. Conference on Runtime Verification


colocated at the Computational Logic Autumn Summit (CLAS)
28.-30. Sept. 2022, Tbilisi, Georgia

The 22nd International Conference on Runtime Verification (RV'22), took place as part of the Computational Logic Autumn Summit (CLAS 2022) in Tbilisi, Georgia, from September 28-30, 2022.


Next RV conference: Thessaloniki/Greece, 4-6 October 2023
https://rv23.csd.auth.gr
Organizer: Panagiotis Katsaros


News

  • Awards:
Best Paper Award
Sponsor: Springer
Joshua Schneider, Randomized First-Order Monitoring with Hashing [DOI].
 
Test of Time Award
Sponsor: Toyota
Andreas Bauer, Martin Leucker and Christian Schallhart for their RV'07 paper: The Good, the Bad, and the Ugly, But How Ugly Is Ugly? [DOI].
Award Committee: Y.Falcone, D.Fisman, T.Henzinger, D.Peled (award rules).
 
Congratulations to all the authors!

  • Program: see program in EasyChair

  • Accepted Papers: please see the list of accepted papers.

  • Keynote speakers (click to unfold abstracts):

    Serdar Tasiran, Amazon Web Services, US: Runtime Monitoring of Distributed Systems at Amazon Web Services
    Amazon’s Simple Storage Service (S3) is increasingly adopting a “model first” approach, with formal models being first-class artifacts in the software development process. In this approach, we start by model checking or deductively proving that design models of distributed systems provide key properties such as durability or strong consistency. Then, during integration testing, gamma stages, or even in production, we monitor that the implementation code conforms to the design models. This not only detects/prevents implementation errors, but also forces models and implementations to remain in sync, ensuring that the investments in writing and analyzing models continue to pay off. In this talk, I will present several examples of the model-first approach in S3, and challenges of using runtime verification at S3 scale.

    Michal Valko, DeepMind & Inria, France: Learning by Bootstrapping of Latents

    We will discuss self-supervised representation learning and a new paradigm for it based on bootstrapping of latents. We first present BYOL for images, which relies on two neural networks, referred to as online and target, that interact and learn from each other: From an augmented view of an image, we train the online network to predict the target network representation of the same image under a different augmented view. At the same time, we update the target network with a slow-moving average of the online network. While prior methods had intrinsically relied on negative pairs, BYOL achieved a new state of the art without them. We will also describe follow-ups of BYOL that we have explored within DeepMind, BGRL for graphs, MYOW for new uncharted domains such as neural readings, and BraVe for videos. We finally apply the paradigm to reinforcement learning and discuss curiosity-driven exploration when the rewards are sparse or absent. For this setting, we give a brand new algorithm BYOL-Explore that jointly learns a world representation, the world dynamics, and an exploration policy.

    Bio: Michal is a machine learning scientist in DeepMind Paris, tenured researcher at Inria, and the lecturer of the master course Graphs in Machine Learning at l’ENS Paris-Saclay. Michal is primarily interested in designing algorithms that would require as little human supervision as possible. This means reducing the “intelligence” that humans need to input into the system and minimizing the data that humans need to spend inspecting, classifying, or “tuning” the algorithms. That is why he is working in domains that are able to deal with minimal feedback, such as deep reinforcement learning and self-supervised learning. He received his Ph.D. in 2011 from the University of Pittsburgh under the supervision of Miloš Hauskrecht and after was a postdoc of Rémi Munos before taking a permanent position at Inria in 2012 and at DeepMind in 2019.


Objectives and Scope

Runtime verification is concerned with the monitoring and analysis of the runtime behaviour of software and hardware systems. Runtime verification techniques are crucial for system correctness, reliability, and robustness; they provide an additional level of rigor and effectiveness compared to conventional testing and are generally more practical than exhaustive formal verification. Runtime verification can be used prior to deployment, for testing, verification, and debugging purposes, and after deployment for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair.

The topics of the conference include, but are not limited to:

  • specification languages for monitoring
  • monitor construction techniques
  • program instrumentation
  • logging, recording, and replay
  • combination of static and dynamic analysis
  • specification mining and machine learning over runtime traces
  • monitoring techniques for concurrent and distributed systems
  • runtime checking of privacy and security policies
  • metrics and statistical information gathering
  • program/system execution visualization
  • fault localization, containment, resilience, recovery and repair
  • systems with learning-enabled components
  • dynamic type checking and assurance cases
  • runtime verification for autonomy and runtime assurance

Application areas of runtime verification include cyber-physical systems, autonomous systems, safety/mission critical systems, enterprise and systems software, cloud systems, reactive control systems, health management and diagnosis systems, and system security and privacy.

Please see the Call for Papers for details.

The RV 2022 conference is sponsored by:

Markdown Monster icon

Markdown Monster icon

Toyota