RV-Match logo 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

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.

company mission and vision news team careers publications presentations videos faq Embedded Systems Blockhain Advisory Services Smart Contract Verification Protocol Verification Formal Design and Modeling The IELE Virtual Machine Partnerships contact media kit blog