Runtime verification at work: A tutorial

Philip Daian, Dwight Guth, Chris Hathhorn, Yilong Li, Edgar Pek, Manasvi Saxena, Traian Florin Şerbănuţă, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We present a suite of runtime verification tools developed by Runtime Verification Inc.: RV-Match, RV-Predict, and RV-Monitor. RV-Match is a tool for checking C programs for undefined behavior and other common programmer mistakes. It is extracted from the most complete formal semantics of the C11 language and beats many similar tools in its ability to catch a broad range of undesirable behaviors. RVPredict is a dynamic data race detector for Java and C/C++ programs. It is perhaps the only tool that is both sound and maximal: it only reports real races and it can find all races that can be found by any other sound data race detector analyzing the same execution trace. RV-Monitor is a runtime monitoring tool that checks and enforces safety and security properties during program execution. Our tools focus on reporting no false positives and are free for non-commercial use.

Original languageEnglish (US)
Title of host publicationRuntime Verification - 16th International Conference, RV 2016, Proceedings
EditorsYliès Falcone, César Sánchez
Number of pages22
ISBN (Print)9783319469812
StatePublished - 2016
Event16th International Conference on Runtime Verification, RV 2016 - Madrid, Spain
Duration: Sep 23 2016Sep 30 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10012 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other16th International Conference on Runtime Verification, RV 2016

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Runtime verification at work: A tutorial'. Together they form a unique fingerprint.

Cite this