Runtime Verification Inc. is a startup company aimed at using runtime verification-based techniques to perform security audits on virtual machines and smart contracts on public blockchains. It is dedicated to using its dynamic software analysis approach to improve the safety, reliability, and correctness of software systems in the blockchain field.
For the time being, blockchain safety tests are mostly lightweight static analysis tests (testing only the internal logic of source code), while dynamic analysis test (using the data generated as the codes are compiled and executed) increases coverage to find bugs as opposed to static analysis tests. Runtime Verification is a global leader in formal verification and is capable of directly verifying compiled binary code. Compared to the formal verification of source code, this catches bugs that are otherwise missed due to miscompilation.
Our headquarters is located in Champaign-Urbana, Illinois, a short distance away from the University of Illinois campus.
What is runtime verification?
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.
Why runtime verify?
Runtime verification is a software development best practice which has the ability to help your team achieve:
Increased standards compliance: strong assurance of compliance is possible
Less effort spent tracking the most subtle bugs, saving development and testing cost
Increased coverage to find tricky bugs that traditional testing or static analysis may not
The ability to check custom properties together with generic, universal properties
How is runtime verification different?
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.
