Finding $\forall\exists$ Hyperbugs using Symbolic Execution
Arthur Correnson, Tobias Niessen, Bernd Finkbeiner, Georg Weissenbacher
TL;DR
This work tackles the challenge of verifying forall-exists hyperproperties, which require, for every execution, the existence (and non-existence) of related traces. It introduces a fully automated approach that extends symbolic execution with trace quantification in the fragment $ extrm{OHyperLTL}_ ext{safe}$, using a bounded semantics to manage terminating and non-terminating behaviors. A lazy, scalable algorithm—supported by an asynchronous product construction—computes symbolic encodings of bounded hyperproperties and can generate concrete counterexamples without user guidance. Empirical evaluation on public and new benchmarks shows the method effectively identifies hyperproperty violations across infinite-state reactive programs, often faster than existing tools, and without requiring loop invariants. This advances automated hyperbug detection and provides a practical pathway toward scalable analysis of complex relational properties.
Abstract
Many important hyperproperties, such as refinement and generalized non-interference, fall into the class of $\forall\exists$ hyperproperties and require, for each execution trace of a system, the existence of another trace relating to the first one in a certain way. The alternation of quantifiers renders $\forall\exists$ hyperproperties extremely difficult to verify, or even just to test. Indeed, contrary to trace properties, where it suffices to find a single counterexample trace, refuting a $\forall\exists$ hyperproperty requires not only to find a trace, but also a proof that no second trace satisfies the specified relation with the first trace. As a consequence, automated testing of $\forall\exists$ hyperproperties falls out of the scope of existing automated testing tools. In this paper, we present a fully automated approach to detect violations of $\forall\exists$ hyperproperties in software systems. Our approach extends bug-finding techniques based on symbolic execution with support for trace quantification. We provide a prototype implementation of our approach, and demonstrate its effectiveness on a set of challenging examples.