Traditional separation logic-based shape analyses utilise inductive summarising predicates so as to capture general properties of the layout of data-structures, to verify accurate manipulations of, e.g., various forms of lists or trees. However, they also usually abstract away content properties, so that they may only verify memory safety and invariance of data-structure shapes. In the first part of this talk, we introduce a novel abstract domain to describe sequences of values of unbounded size, and track constraints on their length and on extremal values contained in them. We define a reduced product of such a sequence abstraction together with an existing shape abstraction so as to infer both shape and content properties of data-structures. We report on the implementation of the sequence domain, its integration into a static analyser for C code, and we evaluate its ability to verify partial functional correctness properties for list and tree algorithms. In the second part, we consider application of this static analysis framework to the verification of the functional correctness of an OS micro-kernel. Our verification method inputs the global invariant of the operating system (data-structures and consistency conditions) and carries out automatic static analysis for each system call to verify preservation of the global invariant.

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.