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.

Initial architects envinsioned RDF as a knowledge representation language, freeing users from syntactic limitations and revolutionizing the way information was exchanged.
While inference and description logic are applied to RDF, the foundation of simple assertions composed of global, unambiguous identifiers, has many more mondane and practical applications.
Distributed contributions to large (web-scale) data graphs demands adaptation of tree and stream-based validation techniques to operate over a graph.
Shape Expressions performs an ordered traversal of RDF graphs to
1 validate of structural constraints.
2 perform generative semantic actions.