Seminars

Abstract: Separation logic is used as an assertion language for
Hoare-style proof systems about programs with pointers,
and there is an ongoing quest for understanding its
complexity and expressive power. There are also
a lot of activities to develop verification methods
with decision procedures for fragments of practical use.

Actually, there exist many variants for separation
logic that can be viewed as fragments of second-order logic,
as well as variants of modal or temporal logics in which
models can be updated dynamically.

In this talk, after introducing first principles on separation logic,
issues related to decidability, computational complexity and expressive
power are discussed. We provide several tight relationships with
second-order logics, interval temporal logics or data logics, depending
on the variants of the logic and on the syntactic resources available.