  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 $\forall^k\exists^l$ 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 $\forall^k\exists^l$ 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.
