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 a 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.

Prof. Xavier Rival’s research focus is on static analysis for the verification of semantic properties of programs. His work is on abstract interpretation and more specifically on symbolic abstractions. He is the director of the Computer Science Department at Ecole Normale Superieure, Paris, France. He is also a Research Director at INRIAS Paris, Head of the ANTIQUE(ANayste staTiQUE) Project.