HYPER 2026

TBA

Many important functional and security properties—including non-interference, determinism, and generalized non-interference (GNI)—are hyperproperties, i.e., properties relating multiple executions of a program. Existing separation logics allow one to reason about specific classes of hyperproperties, e.g., ∀∀-hyperproperties such as non-interference and ∃∃-properties such as non-determinism. However, they do not support quantifier alternation, which is for instance needed to express GNI. The only existing logic that can reason about such properties is Hyper Hoare Logic, but it does not support heap-manipulating programs and, thus, is not applicable to common imperative programs.

This paper introduces Hyper Separation Logic (HSL), the first program logic that supports modular reasoning about hyperproperties with arbitrary quantifier alternation over programs that manipulate the heap. HSL generalizes Hyper Hoare Logic with a novel hyper separating conjunction that lifts the standard separating conjunction to sets of states, enabling a generalized frame rule for hyperproperties. We prove HSL sound in Isabelle/HOL and demonstrate its expressiveness for hyperproperties that lie beyond the reach of existing separation logics.

Heisenbugs—a pun on the name of Werner Heisenberg—are bugs that alter their behavior or disappear when attempts are made to find and analyze them. Such bugs occur in a range of contexts including elusive concurrency bugs as well as unintended system alterations during debugging, and can be caused by various sources of nondeterminism on different system levels. We frame Heisenbugs and their causes as twosafety hyperproperties, thus providing formal foundations for rigorously reasoning about causes of Heisenbugs, and making this challenging class of bugs amenable to an arsenal of existing tools and techniques.

Hyperproperties, properties that relate sets of execution traces rather than a single one, are needed to express information-flow security policies like noninterference, consistency criteria like linearizability, robustness in cyber-physical systems, and diagnosability, none of which can be captured by standard trace logics.

Since HyperLTL and HyperCTL* equipped LTL and CTL* with explicit, simultaneous quantification over traces, the area has grown into a small zoo of logics, semantics, and verification techniques.

In this talk I will take a chronological tour of that landscape, starting from the original synchronous hyperlogics and their automata-based and reduction-based model-checking algorithms, then follow two threads: time, including discrete and pointwise timed semantics (HyperMTL) and finite-trace semantics with past operators; and asynchrony, including traces that stutter or advance along independent contexts or trajectories (HyperLTL_S, HyperLTL_C, A-HLTL), undecidability in general but with decidable fragments, and recent attempts to unify these extensions into a single framework. I will also look at non-standard semantics, from multimodels to what these logics express when evaluated for a single trace model, where some asynchronous fragments turn out to characterize non-regular properties.

From the algorithmic side, we move from automata constructions and self-composition reductions to bounded model checking via QBF and SAT, with an eye on the elusive loop conditions; and from static verification to gray-box runtime verification. I will close the talk by looking past finite-state systems, e.g. population protocols, with some thoughts on open problems.

We report on further investigations into the expressive power of logics for hyperproperties, namely the relationship between HyperLTL and the polyadic μ-calculus. We establish the existence of properties that is not definable in HyperLTL but in the polyadic μ-calculus. By reinvestigating the proof of PSPACE-, resp. EXPSPACE-hardness of fragments of HyperLTL of small quantifier alternation depth, we seek to find simple patterns of HyperLTL formulas that cannot be expressed in the polyadic μ-calculus.

We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.

Formal specification is a powerful tool to guide the learning process and provides significant advantages over reward shaping: (1) mathematical rigor; (2) expressiveness to specify objectives and constraints, and (3) the ability to define tactics to achieve objectives. However, these benefits remain largely unexplored in the context of Multi-Agent Reinforcement Learning (MARL). This talk introduces HyPOLE, a novel framework for MARL under partial observability, where learning is guided by the expressive power of the so-called hyperproperties and, in particular, the temporal logic HyperLTL. We integrate Centralized Training for Decentralized Execution (CTDE) techniques with HyPOLE to synthesize decentralized policies, and our evaluation on Starcraft II and WildFire benchmark demonstrates clear advantages over baselines.

There are two main contenders for a grand unified theory of computer security: hyperproperties in the formal methods community, and the Real–Ideal paradigm (e.g., Universal Composability) in the cryptography community. I describe how they meet in the Viaduct compiler, which transforms high-level sequential programs to distributed, concurrent cryptographic realizations. Even though the source and target systems have very different properties, the Viaduct compiler transformation preserves the security promises of the original source program, because it robustly preserves all hyperproperties. The proof of Robust Hyperproperty Preservation is achieved by building a series of Real–Ideal simulations that transitively connect the source to the final target. This work points to a deep connection between these two contending perspectives, and suggests that Real–Ideal simulations are a powerful tool for security specification and provable enforcement.

Language containment plays an important role in fast model checking for hyperproperties. In the literature, many algorithms exist to check language containment between finite-state automata. Instead of algorithms, in this talk, we focus on deductive systems for language containment. Deductive systems have two advantages: First, they can be used to produce a certificate for language inclusion. Second, deductive systems can also reason about infinite-state systems, which allows reasoning about programs for example. We present a deductive system which allows interactively proving language containment based on fair simulation with the help of a proof assistant.

So far, the verification of reactive systems against temporal hyperproperties has been mostly studied from the perspective of model-checking for finite-state systems (e.g., hardware). However, there is still a lack of interactive and deductive techniques to prove temporal hyperproperties of infinite-state systems (e.g., software). This presentation aims to give an introduction to recent works based on cyclic deductive proof system for verifying temporal hyperproperties with the help of an interactive proof assistant. In particular, we will present HyCo, a framework for the interactive verification of ∀*∃*-safety properties embedded in the Rocq proof assistant.

Information flow security ensures that the secret data manipulated by a program does not influence its observable output. In concurrent programs, operations on secret data may influence the execution time of a thread and, thereby, the interleaving between threads; such internal timing channels may affect the observable outcome of a program even if an attacker does not observe execution times. Existing verification techniques attempt to prove that secret data does not influence the relative timing of threads. However, these techniques are often restrictive (forbidding branching on secrets) and make strong assumptions about the execution platform (ignoring caching and other common features that affect execution time).

In this talk, we will give an overview of CommCSL, a verification technique for secure information flow in concurrent programs that lifts these restrictions and does not make any assumptions about timing behavior. We will explain its key idea, which is to prove that all mutating operations performed on shared data commute, such that different thread interleavings do not influence its final value. Subsequently, we will describe some limitations of CommCSL in its current form and outline ideas on how they can be addressed.

Some security properties of cryptographic protocols cannot be expressed as trace properties. This is typically the case for privacy-related properties such as anonymity, or unlinkability. They are generally expressed in terms of an adversary's inability to distinguish two distinct scenarios, while actively interacting with the protocol. In symbolic models (following the initial work of Dolev and Yao) such indistinguishability properties can be naturally modeled using process equivalences in extensions of the pi calculus such as the applied pi calculus.

We will illustrate how process equivalences can be used to model privacy properties. We provide complexity results for the underlying verification problem (when the number of sessions is bounded) and we will describe the decision procedure underlying the DeepSec verification tool.

We introduce Disintegration Temporal Logic (DTL), a new probabilistic temporal logic that can express a wide range of probabilistic hyperproperties, including probabilistic non-interference and perfect indistinguishability. DTL is based on the notion of measure disintegration from probability theory, which allows for conditioning probabilities on a finite or infinite sequence of events occurring during a program execution. We relate the new logic to existing concepts, such as distributional transformers for Markov decision processes, probabilistic automata on infinite words, and existing probabilistic logics. While model checking Markov chains against full DTL is undecidable, we identify two decidable fragments that capture many hyperproperties of interest. The qualitative fragment is handled by an automata-theoretic procedure that extends the standard algorithm for HyperCTL* with reasoning about the bottom strongly connected components. The linear fragment admits a polynomial-time model-checking procedure based on linear algebraic techniques.

This work investigates the affine segment decomposition algorithm used in the Rocq-NN-Roll prover for neural network hyperproperties through the lens of monoidal categories. This perspective is designated for future integration into Rocq-NN-Roll to facilitate reasoning.

This talk presents HyperLasso, the first symbolic bounded model checker for ∀+∃+ HyperLTL properties with liveness constraints over arbitrary reactive systems. Existing symbolic approaches handle only safety hyperproperties or arbitrary properties over terminating systems, while explicit-state tools support the full logic at the cost of severe state explosion. As a result, certain versions of properties like generalized non-interference, self-stabilization, robustness, and several synthesis problems have remained beyond the reach of scalable symbolic methods.

The key challenge is that refuting such properties requires reasoning about infinite, lasso-shaped executions: a witness found within a certain bound may be spurious if the corresponding universal counterexample appears only at a larger bound. We address this by combining a bounded search procedure that synthesizes candidate counterexamples with a separate checker that validates them against the full system. Experimental results show substantial scalability improvements over existing complete explicit-state approaches while retaining support for arbitrary reactive systems.