Monitoring and Predicting with RV-Monitor and RV-Predict
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.