# RVHyper: A Runtime Verification Tool for Temporal Hyperproperties

arXiv: https://arxiv.org/abs/1906.00798 · HTML: https://mlsanity.com/paper/1906.00798/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 31 May 2019.

## Built on by (most cited first, 1 of 1)

- [Monitoring Second-Order Hyperproperties](https://mlsanity.com/paper/2404.09652/) (2024)

## Abstract (arXiv)

We present RVHyper, a runtime verification tool for hyperproperties. Hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other. Specifications are given as formulas in the temporal logic HyperLTL, which extends linear-time temporal logic (LTL) with trace quantifiers and trace variables. RVHyper processes execution traces sequentially until a violation of the specification is detected. In this case, a counter example, in the form of a set of traces, is returned. As an example application, we show how RVHyper can be used to detect spurious dependencies in hardware designs.