RV-Match

Get to market faster, increase code portability, and save on development and debugging with the most advanced and precise semantics-based bug finding tool.

RV-Match gives you

an automatic debugger for subtle bugs other tools can't find, with no false positives
seamless integration with unit tests, build infrastructure, and continuous integration
a platform for analyzing programs, boosting standards compliance and assurance

Read the Documentation Download RV-Match

Based on cutting edge research and a complete formal ISO C11 semantics, RV-Match generates powerful, rigorous, and automatic tools for analyzing your codebase, including undefinedness. And with no false positives, developers waste no time in their workflow.

When and why should I use RV-Match?

While RV-Monitor can verify and enforce compliance to certain properties for a given execution of a program, RV-Match can prove the correctness of a program at runtime, analyzing the execution trace on all possible execution paths and over all possible inputs. RV-Match provides strong correctness guarantees, leveraging a formally defined semantics of the target language to simulate execution symbolically. RV-Match should be used when the strong guarantees of formal verification are desirable, and can also be used together with RV-Monitor to remove monitoring in areas where properties are provably never violated.