HyperMonitor: {A} Python Prototype for Hyper Predictive Runtime Verification

We present HyperMonitor a Python prototype of a novel runtime verification method specifically designed for predicting race conditions in multithread programs. Our procedure is based on the combination of Inductive Process Mining, Petri Net Tranformations, and verification algorithms. More specifically, given a trace log, the Hyper Predictive Runtime Verifier (HPRV) procedure first exploits Inductive Process Mining to build a Petri Net that captures all traces in the log, and then applies semantic-driven transformations to increase the number of concurrent threads without re-executing the program. In this paper, we present the key ideas of our approach, details on the HyperMonitor implementation and discuss some preliminary results obtained on classical examples of concurrent C programs with semaphors.