Hyperproperties specify the behavior of a system across multiple executions, and are an important extension of regular temporal properties. Most algorithms for deciding if a given system satisfy a given hyperproperty rely on a user-specified abstraction of the system. In this work, we suggest a novel automatic abstraction-refinement algorithm for hyperproperties verification. Our approach is based on predicate abstraction and the recently introduced reduction of hyperproperties verification to satisfiability of Constrained Horn Clauses (CHCs).
Moreover, it formalizes and uses CHC-based refinement for counterexamples in the shape of a directed acyclic graph. We implemented our new algorithm on top of the SMT solver Z3. Our experimental evaluation shows our automatic abstraction refinement algorithm can solve a variety of hyperproperty verification problems, completely automatically. This is in contrast to other existing techniques that require a user-given abstraction.