Embedded systems
Formal methods for software that ships inside hardware
Proving programs correct across every path, enforcing the properties you care about at runtime, and catching the data races testing never reaches. The RV-* toolkit below is archived; the discipline behind it is still the work.
These three tools are archived. They are documented here because the research behind them is still cited and the code is still public, but they are no longer developed or supported.
RV-Match
ArchivedExhaustive runtime verification performed symbolically on all possible program paths, proving properties correct for every execution of a given program. Get to market faster, increase code portability, and save on debugging.
Read about RV-Match
RV-Monitor
ArchivedA development methodology and library generation tool for monitoring and enforcing properties you select, at runtime. Check your code against the Java API, or against custom specifications of your choice.
Read about RV-Monitor
RV-Predict
ArchivedPredictive runtime analysis that automatically detects the rarest and most difficult data races in Java and C/C++ code, with the most precise race finder available.
Read about RV-PredictPartners and customers
From the blog
Writing on embedded systems.
Runtime Verification Launches a Registered Algorand Relay Node
We are thrilled to announce that Runtime Verification has launched a new registered Algorand relay node, contributing to the operation of Algorand’s network
RV-Match now supports inline assembly
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Undefined Behavior Review: tis-interpreter vs. RV-Match
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
C11 Fails to Define Data Races Involving Interrupts
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Building something that has to run correctly every time?
Work with us