runtime verification

Easy runtime verification. Simple static analysis.

Enforce safety policies, detect policy violations at runtime, find race conditions, and more.



Runtime Verification is a new startup providing simple solutions to analyze your team's code through cutting-edge program verification research. Our tools are entirely automatic, generate no false positives, and integrate easily into your team's existing workflow.



We offer the best possible solutions for reliable software development and analysis developed by leaders in the runtime monitoring community. With both generic products and customized support, let us help improve your codebase today.



Core Technologies



RV Monitor


RV Monitor provides light weight formal analysis tools to verify the correctness of a program's execution as it runs. After defining safety properties formally in one of several simple provided logics (including extended regular expressions, finite state machines, and linear temporal logic), RV Monitor generates a native library to instrument and monitor your code automatically, reporting and recovering from errors. This allows for the safety properties of the application and their enforcement to be separate from the native code, easing development and testing.


RV Predict


RV Predict allows for the detection of data races and atomicity violations in concurrent Java programs. RV Predict requires no configuration and runs entirely automatically, analyzing the execution trace of the monitored program for potential errors. Unlike tools based on static analysis, RV Predict does not detect false positives. With a high detection rate, RV Predict will find bugs in complex programs even if they are not encountered during execution, and has been used to find data races in Eclipse and other open projects.


RV Match


RV Match is an upcoming product that provides full program verification through exhaustive semantics-based symbolic execution. RV Match is the most formal of the RV tools, allowing for the generation of proof certificates for any property in any language whose semantics are defined. RV Match will explore the the entire possible state space of a program, providing guarantees which are much more formally rigorous and complete than those provided by RV Monitor. Its ease of use and flexibility bring strong formal guarantees to the enterprise.

Ecosystem


We also develop several specialized tools around our core technologies.

RV Android provides a framework for the instrumentation and monitoring of Android applications using libraries generated by RV Monitor.
property-db is a self-contained database of over 200 formalized safety properties of the Java API for use with RV Monitor.

The open source community is important to us. You can view and contribute to RV projects on Github.