# Software Verification of Hyperproperties Beyond k-Safety

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Jun 2022.

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

- [Non-Deterministic Planning for Hyperproperty Verification](https://mlsanity.com/paper/2405.13488/) (2024)
- [Deductive Controller Synthesis for Probabilistic Hyperproperties](https://mlsanity.com/paper/2307.04503/) (2023)
- [On Conformant Planning and Model-Checking of exists^*forall^* Hyperproperties](https://mlsanity.com/paper/2512.23324/) (2025)

## Abstract (arXiv)

Temporal hyperproperties are system properties that relate multiple execution traces. For (finite-state) hardware, temporal hyperproperties are supported by model checking algorithms, and tools for general temporal logics like HyperLTL exist. For (infinite-state) software, the analysis of temporal hyperproperties has, so far, been limited to k-safety properties, i.e., properties that stipulate the absence of a bad interaction between any k traces. In this paper, we present an automated method for the verification of forallkexistsl-safety properties in infinite-state systems. A forallkexistsl-safety property stipulates that for any k traces, there exist l traces such that the resulting k+l traces do not interact badly. This combination of universal and existential quantification enables us to express many properties beyond k-safety, including, for example, generalized non-interference or program refinement. Our method is based on a strategy-based instantiation of existential trace quantification combined with a program reduction, both in the context of a fixed predicate abstraction. Notably, our framework allows for mutual dependence of strategy and reduction.