Runtime Verification

Runtime Verification Inc. is a startup company aimed at using runtime verification-based techniques to improve the safety, reliability, and correctness of software systems. We are founded and staffed by pioneers and leaders in the runtime verification field, with over 100 publications and related tools that shaped the field.

Our headquarters is located in Champaign-Urbana, Illinois, a short distance away from the University of Illinois campus.

Runtime verification is a dynamic software analysis approach that analyzes programs as they execute, observing the results of the execution and using those results to find bugs.

Runtime verification relies on certain properties that the execution of the program should not violate. Some of these properties, like a lack of data races in a concurrent program, are universal and can be checked automatically. Other properties, like the specification for a proprietary library, are custom to a specific application or purpose. Runtime verification can check universal properties automatically, requiring no development input, and can check any custom properties expressed formally by developers.

Runtime verification can be more lightweight than traditional formal analysis techniques, like model checking or deductive verification. Because runtime verification considers only the execution of the system and not its code, it is possible to rigorously find bugs while scaling to large codebases. Runtime verification is also more precise than lightweight static analysis techniques, which often make simplifying assumptions or use imprecise heuristics to analyze code, leading to false positives which can frustrate developers and testers.

Runtime verification is not meant to replace traditional unit-based, functional, and integration testing, or even lightweight static analysis tools. We believe runtime verification is a good complement to these techniques, providing high confidence in the robustness of application behavior traditionally reserved for complex and inaccessible formal methods techniques while remaining practical and scaling to large codebases.