Runtime Verification provides cutting-edge technology to design safe and secure systems and languages based on mathematically-grounded principles. Runtime Verification technology automatically and accurately detects the rarest, trickiest and most costly bugs lurking in your existing codebase or specifications.
K is a formal semantics framework for defining and designing programming languages and program analysis and verification tools for them.
RV-Match is a semantics-based dynamic analysis tool and debugger for C errors, and an automatic checker for all C undefinedness.
RV-Predict is an automatic predictive runtime analysis tool that detects a variety of Java and C concurrency errors without any false alarms.
|Dec 15 2017||IELE: A New Virtual Machine for the Blockchain|
|Dec 14 2017||RV Inc. & FSL @ UIUC Release First Formal Viper Tools|
|Dec 06 2017||ERC20-K: Formal Executable Specification of ERC20|
|Oct 25 2017||New Technologies for the Blockchain: IELE (virtual machine) and K (universal language framework)|
|Oct 19 2017||RV Inc. & FSL @ UIUC to Formalize Ethereum’s Viper|