Dynamic Resources and Separation and Update Logics – DynRes

What society expects from computer systems is simply that they work
correctly and that they warrant quality, since an error can have
devastating effects. In order to deal with the complexity and the
heterogeneity of these systems there is a need for formal frameworks
that integrate, in a global way, the possible interactions between the
computability models and the constraints issued from their physical
environment. In this context, one main problem about heterogeneity is
the definition of composition operators that are sufficiently generic
to be applied to large domains but with preservation of a coherent
semantics for the composed entities. Moreover there is a need of
theories that allow the integration of components in a semantically
coherent way. A well-known logical formalism to express local
properties in memory states is Separation Logic (SL) that allows
reasoning about mutable data structures. SL provides an actual way of
understanding the separating conjunction and implication in the
perspective of local reasoning on mutable data structures like
pointers and memory. From a semantic point of view, the models of SL
are very specific models of so-called BBI with classical additives,
that validate the axioms for Hoare triples. Separation Logic allows to
express particular properties about programs that manipulate
dynamically-allocated linked data structures and to verify such
properties in these specific models. Although SL remains an
interesting subject of study, it has some limitations: its models are
very specific and concrete models of computer storage and it can be
viewed as a specification language expressing properties that should
be verified or not in a specific model. Thus the specification and
verification are developed in a too restricted model of separation and
update. Moreover the resource properties expressed in SL are mainly
static and there is no proof theory is known for Separation Logic and
its variants.

There exist various logics and resource models, related to Separation
Logic that are based on particular structures like different kinds of
trees and graphs They mainly depart from SL by
modifying the axioms for separation, thus deriving ad-hoc structures
matching a particular aspect of the notion of resource
composition. They sometimes include attemps to consider update with
separation but the ways to deal with it are ad-hoc w.r.t. structures
and then have limitations in the context of specification and
theorem-proving. Thus we consider update logics that have been
recently studied to model data structures and their evolution and aim
at developing them in the context of Separation Logic in order to deal
with dynamics resources.

Our main goal is to study the foundations of new resource models, and
related logics, having in mind that SL is only a particular
case. Reasoning about resources and their evolution is essential to
design systems (networks, servers) or programs that access memory and
manipulate data structures. In this perspective we aim at studying
new resource models and logics for separation and update dedicated to
specification and theoremproving with decision procedures focusing on
generation of proofs, refutations and plays obtained from dedicated
games.
The subject of separation and update of resources is an important
topic for which the recent results on separation, tree and context
logics are promising with impact on applications like memory,
permissions and other structure management. Thanks to the expertise of
the different partners from IRIT, LORIA and LSV, we propose a global
treatment for reasoning about resources from the foundations of
resource models to the design of logics, proof systems and
implementation of decision procedures.