Many important hyperproperties, such as refinement and generalized non-interference, fall into the class of ∀∃ 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 ∀∃ 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 ∀∃ 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 ∀∃ hyperproperties falls out of the scope of existing automated testing tools. In this paper, we present a fully automated approach to detect violations of ∀∃ 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.

@article{CorrensonNFW24,
  title = {Finding ∀∃ Hyperbugs using Symbolic Execution},
  author = {Arthur Correnson and Tobias Nießen and Bernd Finkbeiner and Georg Weissenbacher},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {OOPSLA2},
  year = {2024},
  doi = {10.1145/3689761}
}