# Automated Software Verification of Hyperliveness

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Mar 2024.

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

- [Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI](https://mlsanity.com/paper/2608.00882/) (2026)

## Abstract (arXiv)

Hyperproperties relate multiple executions of a program and are commonly used to specify security and information-flow policies. Most existing work has focused on the verification of k-safety properties, i.e., properties that state that all k-tuples of execution traces satisfy a given property. In this paper, we study the automated verification of richer properties that combine universal and existential quantification over executions. Concretely, we consider forallkexistsl properties, which state that for all k executions, there exist l executions that, together, satisfy a property. This captures important non-k-safety requirements, including hyperliveness properties such as generalized non-interference, opacity, refinement, and robustness. We design an automated constraint-based algorithm for the verification of forallkexistsl properties. Our algorithm leverages a sound-and-complete program logic and a (parameterized) strongest postcondition computation. We implement our algorithm in a tool called ForEx and report on encouraging experimental results.