The Taub Faculty of Computer Science Events and Talks

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. Affiliation: CISPA Helmholtz Center for Information Security. Short bio: Hadar Frenkel is a postdoctoral researcher at CISPA Helmholtz Center for Information Security in Saarbrücken, Germany, hosted by Prof. Bernd Finkbeiner. She obtained her PhD from the Technion in 2021, under the supervision of Prof. Orna Grumberg and Dr. Sarai Sheinvald. Hadar studies complex hyperproperties, such as knowledge, causality, and asynchronous hyperproperties, and searches for logical formalisms and verification algorithms for them. She also studies automata learning and its applications in program verification and repair.