|
Main /
ProposalWhat 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. In this perspective, rules of compositionality and of interference control must be provided, the former ensuring that local properties of sub-systems are preserved by incremental construction and the latter ensuring the inference of global properties from local properties of sub-systems. 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 several 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 Separation Logic 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. Indeed, resources are central in computer science and the concepts of ownership, access, separation, consumption are important for resources. In this perspective we aim at studying new resource models and logics for separation and update dedicated to specification and theorem proving with decision procedures focusing on generation of proofs, refutations and plays obtained from dedicated games. It corresponds to a general and foundational study of separation and update of resources from two non-explored but challenging research directions: the specification of systems and resource properties and their verification through the construction of proofs and refutations usable in the process of system developments. 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. |