Hadar Frenkel - Verification of Complex Hyperproperties

Hyperproperties are system properties that relate multiple execution traces to one another. Hyperproperties are essential to express a wide range of system requirements such as information flow and security policies; epistemic properties like knowledge in multi-agent systems; fairness; and robustness. 
With the aim of verifying program correctness, the two major challenges are (1) providing a specification language that can precisely express the desired properties; and (2) providing scalable verification algorithms. 
In this talk, I will give an overview of my recent work on addressing these two challenges. 
First, I will present the new logic Hyper^2LTL, which uses second-order quantification over sets of executions to express a wide range of complex hyperproperties such as common knowledge in multi-agent systems and asynchronous hyperproperties.
Second, I will present a (sound but necessarily incomplete) model-checking algorithm for Hyper^2LTL; While the verification of Hyper^2LTL is undecidable, we manage to handle undecidability by characterizing a rich fragment of the logic that allows for sound approximations, providing the first verification algorithm for Hyper^2LTL specifications. 
Last, I will outline my work on causal analysis in reactive systems, both in formalizing causality to the setting of reactive systems and infinite executions and in algorithms for verifying and generating explanations.