Title: Towards Incrementalization of Holistic Hyperproperties

Abstract: 

A hyperproperty is a set of sets of finite or infinite traces over some fixed
alphabet and can be seen as a very generic system specification. As originally
defined, hyperproperties are easily specifiable but difficult to reason about.
Therefore, in this talk an alternative, incremental view on system
specification and verification is presented. Firstly, a formal classification
of hyperproperties into holistic and incremental ones is introduced.  Secondly,
the notion of incrementalization, a transformation to convert holistic
specifications into incremental ones, is presented and illustrated on
particular classes of hyperproperties. Finally, a possible verification
methodology for incremental hyperproperties is presented.  In conclusion, this
work can be seen as a step towards a generic verification methodology for
(classes of) hyperproperties.