Monitoring and Predicting with RV-Monitor and RV-Predict

Grigore Rosu / Persyval-Lab

RV-Monitor and RV-Predict are two recent runtime verification systems developed by Runtime Verification, Inc. (http://runtimeverification.com), which incorporate and significantly extend runtime verification technology developed at the University of Illinois at Urbana-Champaign, such as JavaMOP and jPredict.  This talk will present these systems in detail.  RV-Monitor is an efficient monitoring library generator for parametric properties.  A novel implementation of JavaMOP using RV-Monitor is also available.  RV-Predict is a concurrency bug detector/predictor, which generates causal models expressed using constraints from program executions and then solves those using constraint solvers, e.g., Z3.  The technique underlying RV-Predict is mathematically proved to generate the maximal causal model for any given execution, that is, no other dynamic detector/predictor can find more concurrency bugs analyzing the same execution trace.