Abstract interpretation-based static analysis aims at computing program properties such as absence of runtime errors, (non)-termination, security properties, and more. Semantic properties of interest may generally be classified into families such as trace properties (including safety and liveness) or hyperproperties. Since the former are simpler to express and prove as they feature sound and complete proof methods, they are also addressed by a comprehensive body of works in static analysis techniques and abstract domains. By comparison, hyperproperties are more difficult to analyse in a precise manner. In this presentation, we recall the main distinctions between each of these classes of properties. We cite several examples of hyperproperties, and illustrate the difficulties to compute them. Finally, we compare several static static analysis techniques to infer specific families of hyperproperties.

Xavier Rival is a Senior Research Scientist (Directeur de Recherche) at INRIA Paris. His research interest focus on abstract interpretation and software verification by static analysis. He is mainly working on symbolic abstractions (trace partitionning abstraction, shape analysis, separation logic and memory abstract domains). He has been involved in the design, implementation and transfer of the Astrée analyser, a static analyser able to verify safety properties on industrial size safety critical softwares. He was the PI of the MemCAD ERC Starting Grant, aiming at the design of a library of abstract domains to describe memory states containing a wide range of complex data structures. He has also been the Head of the ANTIQUE INRIA group from 2012 till 2024, located at ENS Paris and now serves as Department Chair for the CS Department of ENS Paris.