Sep 12 – 14, 2022
Europe/Dublin timezone

RV: where are we?

Sep 12, 2022, 3:00 PM
"Lansdowne" (Clayton Hotel on Burlington Road)


Clayton Hotel on Burlington Road

LPC Refereed Track LPC Refereed Track


Daniel Bristot de Oliveira (Red Hat, Inc.)


RV: Where are we?

Over the last years, I've been exploring the possibility of verifying the Linux kernel behavior using Runtime Verification.

Runtime Verification (RV) is a lightweight (yet rigorous) method that complements classical exhaustive verification techniques (such as model checking and theorem proving) with a more practical approach for complex systems.

Instead of relying on a fine-grained model of a system (e.g., a re-implementation of instruction-level), RV works by analyzing the trace of the system's actual execution, comparing it against a formal specification of the system behavior.

The research has become reality with the proposal of the RV interface [1]. At this stage, the proposal includes:

  • An interface for controlling the verification;
  • A tool and set of headers that enable the automatic code generation of the RV monitor (Monitor Synthesis);
  • Sample monitors to evaluate the interface;
  • A sample monitor developed in the context of the Elisa Project demonstrating how to use RV in the context of safety-critical systems.

In this discussion, we can talk about the steps missing for an RV merge and what are the next steps for the interface. Also, to discuss the needs of safety-critical and testing communities, to better understand what kind of models and what kind of new features they need.


I agree to abide by the anti-harassment policy Yes

Primary author

Daniel Bristot de Oliveira (Red Hat, Inc.)

Presentation materials

Diamond Sponsor

Platinum Sponsors

Gold Sponsors

Silver Sponsors

Speaker Gift Sponsor

Catchbox Sponsor

Video Recording Sponsor

Livestream Sponsor

T-Shirt Sponsor

Conference Services Provided by