NuRV - Assumption-Based Runtime Verification (ABRV)

NuRV is a tool for Runtime Verification (RV). It's developed by the FM unit at Fondazione Bruno Kessler (FBK), Italy.

Features

NuRV supports online/offline Runtime Verification of Linear Temporal Logic (LTL) properties under assumptions given by finite-or infinite-state SMV models.

NuRV can also generate finite-state monitors into standalone monitor code in C, C++, Java, Python, Common Lisp, Prolog and LLVM IR.

NuRV contains all functionalities of nuXmv (version 2.0).

Starting from version 1.7.0, NuRV supports network-based (CORBA-based) monitor server (not available on all supported platforms, e.g. Windows).

Starting from version 1.8.0, NuRV supports monitor code generation with high-level API using scalar variables (NOTE: support of SMV arrays were added in 2.0.0).

Starting from version 1.9.0, NuRV supports code generation of "symbolic monitors" which calls NuRV itself as a dynamic library (both finite- and infinite-state monitors are supported).
NOTE: NuRV 1.9.1 fixed a serious bug in the infinite-state RV algorithm causing wrong monitor outputs for certain (rare) properties.

Starting from version 2.0.0, NuRV supports monitor generation in FMU (Functional Mock-up Unit), following FMI 2.0 and 3.0 standards.

Starting from version 2.1.0, NuRV supports finite-state monitors for models with infinite-domain variables (predicate booleanization), state estimation of the unobservable variables during online monitoring, and FMU generation on Windows.

See the User Manual (version 2.1.0) for more details.

Copyrights and Licenses

NuRV is free for academic uses. Commercial customers and other partners should obtain specific licenses for evaluation/application purposes.

Support

Please send bug reports or feature requests to .

Updated on October 27, 2026