Finding $\forall \exists$ Hyperbugs using Symbolic Execution

Arthur Correnson, Tobias Niessen, Bernd Finkbeiner +1

Many important hyperproperties, such as refinement and generalized non-interference, fall into the class of $\forall \exists$ hyperproperties and require, for each execution trace o…