The central role of information technology in all aspects of our private and professional lives has led to a fundamental change in the type of program properties we care about. Up to now, the focus has been on functional correctness; in the future, requirements that reflect our societal values, like privacy, fairness, and explainability will be far more important. These properties belong to the class of hyperproperties, which represent sets of sets of execution traces and can therefore specify the relationship between different computations of a reactive system. For example, to ensure fairness in a hiring system, we are interested in the hyperproperty that for all pair of executions in which the applicants only differ in sensitive attributes – those that should not be taken into consideration by the hiring system – the final hiring decision is the same.

Our research sets out to develop a unified theory for general hyperproperties. This includes the development of new logics that can capture rich classes of hyperproperties, including information flow policies, causality, and algorithmic fairness; the analysis of the complexity and expressivity of those logics; the construction of algorithms that automatically check if a system satisfies a hyperproperty; the synthesis of systems thats satisfy the desired hyperproperties by construction; and monitoring algorithms that judge the satisfaction of hyperproperties in a running system.