MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the ${\exists }^{\ast }{\forall }^{\ast }$ Fragment

Bernd Finkbeiner, Christopher Hahn, Tobias Hans

Hyperproperties are properties that refer to multiple computation traces. This includes many information-flow security policies, such as observational determinism, (generalized) no…