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

Abstract

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
PublisherSpringer
Pages46-67
Number of pages22
ISBN (Print)9783319469812
DOIs
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

Other

Other16th International Conference on Runtime Verification, RV 2016
Country/TerritorySpain
CityMadrid
Period9/23/169/30/16

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

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

Cite this