ANR DynRes | Main / Context

Context of the proposal

A computer system processes data, stores data, uses resources or presents information. What the society expects from these systems is simply that they work correctly (they satisfy their specifications) and that they warrant quality, since an error can have devastating effects. In order to deal with the complexity and the heterogeneity of the 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. Another key point is the constructivity of systems, i.e. to build complex systems satisfying given constraints from constituents with known properties. This problem of building systems from known components is in general undecidable, and even in some finite cases, too complex to deal with. That is why we must study it in specific contexts characterized by particular constraints, components and composition mechanisms. 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 recent logical formalism to express local properties in memory states is Separation Logic (SL) [Reynolds02] that allows reasoning about mutable data structures like pointers and memory [Ishtiaq&OHearn01,OHearn&Reynolds&Yang01]. Reynolds initially proposed an intuitionistic logic extended with a separation connective * [Reynolds00] and Ishtiaq and O'Hearn then investigated the same approach [Ishtiaq&OHearn01] from the point of view of the logic of Bunched Implications (BI) [OHearn&Pym99, Pym02], which allows a joint and modular treatment of intuitionistic connectives and linear connectives. The resource interpretation of BI's connectives, where * decomposes the current resource into pieces (separation) and its adjoint operator -* talks about new and fresh resource (updates), is central. Separation Logic has been succesfully integrated in impressive tools like bi-abductive SpaceInvader for unannotated C code, Verifast for annotated C code, jStar for Java code, and several tools for toy programming languages better representing some concurrency paradigms, like Smallfoot for Hoare monitors, SmallfootRG for non-blocking concurrency, or Heaphop for copyless message-passing. There is an increasing interest for new models of resources and new forms of local reasoning. In this development process, Separation Logic promoted rather specific models of resources that were driven by the considered case studies.

A better understanding of the foundations of resource models and local reasoning is needed, with important potential benefits. Therefore studies should be conducted on theoretical foundations of resource logics in order to unify all mushrooming resource models (permissions, variables as resources, locks, endpoints, rely-guarantee, deny-guarantee, to quote only few of them...).

Moreover, Separation Logic is only one approach of resource composition, but even more resource models were considered in other BI-like or spatial-like logics. In the specific (memory) models proposed for Separation Logic, the distinction between the classical and intuitionistic interpretation of the logical operators does not introduce much difference [Ishtiaq&OHearn01, Reynolds02]: encoding from one intuitionistic SL into classical SL and vice-versa are provided. But it is important to notice that this property of the specific (memory) model of SL does not extend to the more general class of models of BI, with intuitionistic additives and Boolean BI (BBI), with classical additives [Galmiche&Larchey06, Larchey&Galmiche09]. So, nowadays, Separation Logic is mainly understood with a classical interpretation of its additive connectives. Thus, from a semantic point of view, the models of SL are very specific models of BBI, that validate the axioms for Hoare triples. Such a 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 Separation Logic in its standard understanding is a very interesting formalism, there is a need to extend it, which is witnessed by its limitations related to the concepts of separation and updates. Models of Separation Logic are very specific and concrete models of computer storage where memory cells are organized as heaps and the operation of heap composition (logically interpreted by the * operator) is an aggregation. Other abstract resource models are worth being investigated. Separation Logic 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, reasoning about data or quantitative aspects has been seldom studied for this formalism. Moreover Separation Logic only expresses static properties about memory states and there is no trivial way to extend it to deal with dynamic resources. New resource models including separation but also including management of dynamic resources are needed. Finally there is no proof theory is known for Separation Logic and its variants, which would advantageously complete the existing verification approach mainly based on model-checking techniques.

Questions related to the above limitations have been partly answered in recent past and in this project we aim to be systematic in repairing the main defects from the standard understanding of Separation Logic.

In order to mention recent developments, it is worth recalling that there exist various logics and resource models, related to Separation Logic and its connectives * and -*, that are based on particular structures like ambients and algebraic processes [Cardelli&Gordon00][Cardelli&Ghelli04], different kinds of trees and graphs [Calcagno&Gardner&Zarfaty05] [Biri&Galmiche07,Cardelli&Gardner&Ghelli02, Conforti&Macedonio&Sassone05], processes and resources [Pym&Tofts07]. They mainly depart from the basic ideas from Separation Logic by modifying the axioms required for the * operator, thus deriving ad hoc structures matching a particular aspect of the notion of resource composition. They sometimes include attempts 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.

In order to study updates in the context of separation logics we start by studying update logics, which are logics that were developed in the domain of artificial intelligence and multi-agent systems [Baltag and Moss04,vanDitmarsch&van der Hoek&Kooi07, Balbiani et al.08]. These logics have been recently developed to model data structures and their evolution [Aucher et al.09,Balbiani&Echahed&Herzig10]. We aim at studying them more deeply in the context of Separation Logic and its neighbours in order to deal with dynamics resources.

The main goal of the project is to propose new resource models, enriching those from separation logics, and to study their mathematical structures as well as their related logics based on two essential concepts about resources: separation and updates.

Reasoning about resources and their evolution is essential to design systems (networks, multicore systems, servers) or programs that access memory and manipulate data structures (with the help of pointers). That is why we propose to study new resource models and logics based on the concepts of separation and update that allow management of dynamic resources. The project is schematically divided in three main research directions:

Resources : models and high-level properties. Reasoning about resources and their evolution is essential to design systems (networks, multicore systems, servers) or programs that access memory and manipulate data structures (with the help of pointers). That is why we propose to study new resource models that allow management of dynamic ressources and to consider new properties on data or quantities.
Separation and update with dynamic resources: from expressivity to decidability. We aim at developing extensions or variants of separation logics with different modalities and constraints: locations or places, temporal constraints and also with quantitative properties, recursion or data. In this context the main challenge is the study of the relationship and possible mix between separation and update in order to deal not only with static resources but also dynamic resources. This original task covers several aspects from study of the expressivity to study of decidable logical fragments. Comparing the expressive power of various formalisms, such as the modal logics of updates shall be performed.
Proof systems and decision procedures for separation and update logics. We also aim at developing calculi for reasoning about such logics, including decision procedures based on sequent-style proof systems, automata and games. Reasoning tasks are not restricted to yes-no answers but also to synthesis, for instance with parallel proof and countermodel. Moreover the implementation of decision procedures in the tool LoTREC developed at IRIT shall be done.

The project, with these research directions, covers non-explored but challenging research topics that are the specification of systems and of resource properties and their verification through the construction of proofs and refutations usable in the process of system developments.

As far as we know, no national and international research group has such a global goal even though some of them treat specific aspects in some ad hoc frameworks. From a methodological point of view, we shall also propose original techniques for instance, relating resource logics with modal logics with updates, designing proof systems that build proofs and refutations, characterizing logical problems with new structures and calculi and investigating symbolic representation of models that can be used uniformly for calculi and automata.

Thanks to the expertise of the different partners IRIT (mainly on modal and update logics), LORIA (mainly on separation logics and proof theory) and LSV (mainly on decidability in and complexity) 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.

Our research groups involved in this project are the main specialists in France to fulfill the announced goals, stemming from theoretical foundations of resource models to automated deduction. This would answer to the current limitations observed for separation logic and the treatment of dynamic resources and thus proposes new theoretical foundations (expressiveness, semantics, calculi, decidability, complexity) and new scopes for specification and verification of resource system properties.

State of the art and positionning of the proposal

Let us present the background and the state of the art about existing resource models, the high-level properties we can express in them, the related resource logics dealing with separation and update, and finally the verification techniques based on deduction mecanisms and automata. Before to describe the project following the research directions we have fixed, we present the state of the art that illustrates the relationships between the design of resource models and logics and their use for the specification and verification of resource properties.

Even if SL usually refers to a specific memory model together with a logical language, it appears as a particular case of the Boolean BI logic [Ishtiaq&O'Hearn01] and several other concrete models have been provided for this logical language and its Kripke interpretation: aside from the heap aggregation model which is present in SL, models based on trees such as Spatial Logic [Caires&Cardelli03], Context Logic [Calcagno&Gardner&Zarfaty05] or Resource Trees [Biri&Galmiche07] all give to composition a particular meaning and sometimes specific properties, such as quantifier elimination [Caires&Lozes06]. Despite this variety of interpretations, none of these classes of models corresponds (through the completeness theorem) to a logic for which analytical proof systems have been provided (model-checking based sequent calculi put aside). These models also fail to integrate consumption/production of resources, what Petri nets did for linear logic [Engberg&Winskel90].

On the other hand, analytical proof systems such as sequent calculi [Pym02] and resource tableaux calculus [Galmiche&Mery&Pym05, Larchey&Galmiche09] provide solid proof-theoretical foundations to both BI and Boolean BI. Their corresponding abstract models (partial monoids with or without a partial order) form complete classes and countermodels can be extracted from failed proof-search attempts. However these abstract models include concepts like non-determinism [Galmiche&Larchey06] or invertibility [Larchey08]. But these concepts which seem important or essential for completeness are trivialized in the current concrete models for Boolean BI. Then, we also remark that the current models, both concrete or abstract, lack dynamic concepts that would allow to model evolution of resource sharing and more refined forms of interaction.

There exists various models for resources in the literature from trees with references [Cardelli&Ghelli04], resource trees [Biri&Galmiche03], graphs [Dawar&Gardner&Ghelli07], algebraic processes [Cardelli&Gordon00,Caires&Cardelli03], or models of memory heaps [Ishtiaq&OHearn01]. Results are often obtained for specific classes of resource models and one of the goals in the project is to establish results for more abstract classes of models [OHearn&Pym&Yang04, Galmiche&Larchey06]. In this direction, a unifying spatial logic for concurrency has been proposed in [Hirschkoff&Lozes&Sangiorgi03]. In addition, resource logics, mainly separation and spatial logics, are associated to these models and can be used both to specify properties of resources or resource-based structures and to analyze executions of programs dealing with such structures [Biri&Galmiche07].

Many interesting properties of real-life programs, such as termination or correctness, depend on quantitative aspects of their inputs (e.g., the length of list, the height of a tree). The idea of mixing shape analysis with arithmetic constraints arises from [Zhang&Sipma&Manna04], which extends early work from Nelson and Oppen [Nelson&Oppen80,Oppen80]. Presburger arithmetic is used to express length constraints on recursive data structures which are defined as term algebras via constructors. A decision procedure is given but it only applies to structures that are uniquely generated by constructors, which rules out queues (queues can grow at both ends). Moreover, this work does not fit well in the context of programs with destructive updates. For such programs, [Rugina04] presents a data flow analysis that is able to infer quantitative invariants automatically, but at the expense of being dedicated to tree structures and tree-balancing properties. Related works are based on model-checking [Yavuz-Kahveci&Bultan02] and shape-analysis [Sagiv&Reps&Wilhelm02] in the 3-valued logic framework (which is a weaker theory than Presburger arithmetic) and are limited to lists and node-counting properties. [Berdine&Cook&Distefano&OHearn06] and [Magill&Berdine&Clarke&Cook07] are the first works that extend SL with some kind of approximative quantitative reasoning to tackle termination properties, whereas [Bozga&Iosif&Perarnau08] introduces Quantitative Separation Logic (QSL) as a logic to express exact statements about singly-linked lists and their length. It is undecidable, the only currently known decidable fragment is the purely existential fragment.

The previously mentioned works include some attempts 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. Concerning the study of logics for updates we can recall that these logics were mainly developed in the domain of artificial intelligence and multi-agent systems [Baltag and Moss04,vanDitmarsch&van der Hoek&Kooi07, Balbiani et al.08]. These logics were used originally in order to account for the evolution of the knowledge of a set of agents (including their common knowledge) in a distributed system, being modelled as the update of the agents’ epistemic structures. Later they were extended in order to account also for agents’ preferences and their evolution [vanBenthem&Liu07] [Baltag&Smets08]. It was only recently that it was recognized and exploited that these logics allow more generally to model data structures and their evolution [Aucher et al.09] [Balbiani&Echahed&Herzig10].

Existing works on automatic program verification with Separation Logic and its variants make use of a wide range of techniques: assertion checking, model checking, shape analysis, data flow analysis, abstract interpretation and transition systems, counter automata [Berdine&Calcagno&OHearn04, Weber04, Berdine&Calcagno&OHearn05, Berdine&Cook&Distefano&OHearn06, Distefano&OHearn&Yang06] [Calcagno&Distefano&OHearn&Yang06] Magill&Berdine&Clarke&Cook07, Bozga&Iosif&Perarnau08]. Model-checking has been successfully applied in academic and industrial applications, see [Berard et al01]. It guarantees the outcome of mathematical correctness proofs (when this is possible theoretically). This approach can be implemented by automata-based techniques where both the system and the properties can be encoded as automata from an appropriate class. Surprisingly, the theorem-proving approach is blatantly missing so that, apart recent algorithms based on labels and constraints (that are represented through resource graphs) for BI and SL [Galmiche&Mery05, Galmiche&Mery05a], there exists no decent proof-theory for any of the numerous extensions of SL currently in use (SL with list or tree predicates, SL with Presburger arithmetic, combinations of recursively defined data structures and arithmetic).

Among the approaches to consider proof and refutation construction for Separation Logic and its extensions, a possible one could be based on games but it has not been explored. There are works on games in Ambient logic [Dawar&Gardner&Ghelli04] and BI logic [McCusker&Pym07] but they are not dedicated to the study of provability in these logics. Works about characterizations of provability with games exist for intuitionistic and intermediate logics [Fermüller03] and also for linear logic [Abramsky97] but the study of games for proof search in the perspective of separation and update is a real challenging issue. It consists in providing games with appropriate winning and counter-winning strategies that would give hints on combination of proof and countermodel construction and also on interaction and exchange of information during the proof search process.

Objectives, originality and/or novelty of the proposal

Starting from the observation that Separation Logic and its ad hoc techniques cannot be generalized to other resource models and logics we aim at studying new resource models and logics dedicated to specification and theorem-proving, with some decision procedures focusing on generation of proofs and refutations. In particular, the originality of our approach consists in considering together in the same framework update operations and separation operations that can be applied to many structures that are involved in mutable data structures.

The analysis of works on existing separation models shows that the models and their potentialities are restricted by specific concrete models of memory in which one can mainly express static properties. In our project we are concerned by different resource models that focus on spatiality and separation (heaps, trees, graphs), on temporality (automata) and on execution (processes). They are dedicated to the expression of both static properties (for example about states of memory) and dynamic properties (for example about program execution).

In order to express high-level properties of resources, that could be static or dynamic, an unexplored approach consists in studying in a systematic way the combination of temporal logics and separation logic in order to specify for instance the behaviors of programs with pointers. It is essential to determine which modes of combination allow decidability of the main verification problems and to design new proof techniques and tools that cannot be simple extensions of known automata-based techniques for instance.

Even though the possibility of such a combination is quite natural and promising, it has never been considered so far except preliminary works in [Brochenin&Demri&Lozes07] [Yahavetal03]. It has been shown how to interpret such connectives of logics for separation and update as modalities in some specific modal logics [Calcagno et al.07]. In this context of the use of a modal logic in order to deal with updates in some structures, two modal logics that allow to reason about modifications of graphs have been recently defined [Aucher et al.07]. The first one only involves global modifications in the graph and the second one allows for modifications that are local to states. There is a strong need for calculi dedicated to automated deduction in such modal logics that deal with separation but also with structure updates or modifications. Our starting point for such a study will be semantic structures, like resource graphs only used in BI logic, from which proof search and countermodel generation could be designed in an appropriate way for our new separation/spatial/modal logics. In this context the use of graph modifiers logics that allow to reason on such structures has to be explored in order to propose original and adequate improvements to the proof-search process.

Such proof systems cannot be simple and direct extensions of systems known for separation/temporal/modal logics and thus we need new approaches to deal with specificities of the resource logics.

Therefore we can summarize the main objectives of the project as being the definitions and studies of :

New resource models, derived from various interpretations of the composition and decomposition of resources with focus on spatiality and separation (resources, heaps, trees, graphs), on temporality (automata) and on execution (processes).
New resource logics that are dedicated to separation and update in order to express resource properties that can be static (for example about states of memory) and dynamic (for example about program execution).
New proof systems that capture the specific interactions between separation operators and modalities in these logics.

The above goals are complementary knowing that new resource models and logics are motivated by the expressivity of high-level resource (qualitative and quantitative) properties, including and mixing separation and update but also the adequacy between such models and proof-search procedures. Then the study of decidable fragments and the design of new semantic structures, based on particular resource constraints, from which validity and generation of countermodels can be studied, are also key points.

This project corresponds to an ambitious general and foundational study of separation and update of resources from 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 realization of these ambitious objectives will start from the study and development of some recent results of the project partners that are based on some original approaches and techniques on related topics. Let us mention for instance the study of undecidability results in the context of separation logics from semantics and embeddings ([Larchey&Galmiche10] LORIA), the definition of a temporal logic LTL whose underlying assertion language is the quantifier-free fragment of separation logic and the proofs of decidability results by reducing standard problems for Minsky machines ([Brochenin&Demri&Lozes09] LSV), the definition of a modal logic tailored to describe graph transformations for a class of graphs called termgraphs, that can be used to specify shapes of classical data-structures, e.g. binary trees, circular lists ([Balbiani&Echahed&Herzig10] IRIT).

Each research group has now various experiences, methods and results in the project topics that could be helpful for tackling the mentioned objectives. But in this perspective the consortium will be the place where some recent original specific approaches could be shared in order to define more general new foundations, techniques and methods for separation and update logics and the treatment of dynamic resources.

A long term goal is to provide decidable fragments and decision procedures for a wide range of resource logics, where the term "procedure" should be understood both from the point of view of proof-search and from the point of view of countermodel construction. In other words, the procedures we are aiming at should be able to build proofs as well as refutations.

Let us precise the rationale highlighting the originality and by developing the topics mentioned in the representation of the state of the art (in order to emphasize the improvements and the challenges w.r.t. the existing works and results).

A) Resources : models and high-level properties.

A main objective of the study of abstract resource models is to explore more deeply the links between the logics defined by the Separation Logic model or other resource models based on aggregation and Boolean BI. Abstract models usually arise as the complement to a logical proof-system for which a completeness theorem is provided.

An (abstract) class of structures is singled out and the completeness theorem states that a formula (i.e. a property expressible in the logical language) is fulfilled for every structure of the class if and only if the formula is provable in the given proof-system. Abstract models may be dependent on complicated mathematical constructs and may not be easy to grasp for an engineer. A typical example of abstract model is the phase model for linear logic, i.e. a monoidal structure endowed with a stable closure operator. On the other hand, concrete models are not introduced from proof-theoretical considerations but they usually represent existing data structures based on particular viewpoint in mind. Then, as basic operations of interest are identified on the data-structures, a logical language is designed together with an interpretation of logical formulae on the data-structures and its corresponding basic operations, so that meaningful properties can be expressed with the logic. Automated methods are designed to check that properties are satisfied or not w.r.t. some particular data-structure. SL comes as a typical example of this process. Aggregation/splitting and memory heap are selected as the concepts of interest and the logical operator * is added to classical logic. The Kripke interpretation is extended to * as a way to interpret formulae as properties of memory heaps. The logic BI was later identified as the core logical language at the heart of SL, mainly because of the Kripke semantics of BI which is a kind of generalization of that of SL. But being more abstract, memory heaps do not form a model for BI suitable to derive a completeness theorem. Generally speaking, the concrete model comes first, the logical language, its interpretation and automated methods come as a consequence.

In this context the main aims are:

To integrate notions coming from abstract models (e.g. invertibility, non-aggregation, etc.) or other resource logics (production/consumption of money tokens) into existing or variants of existing resource models with the overall goal of completeness between extended concrete models and corresponding analytical proof-systems.
To integrate temporal aspects into Boolean BI and SL-like logics and propose a framework to model interaction through interleaved and lock-controlled sharing of resources.
To define and study models of interference which abstract the management of locking and deal with high-level concepts such as coherence. A key but difficult point would be to design a model of interference which cannot be reduced to interleaved interaction and locking, thus strictly expanding the existing models of interaction.

Extending the scope of application of separation logic to standard temporal logic-based verification techniques has many potential interests.

The originality of the approach we advocate and for which a first attempt can be found in [Brochenin&Demri&Lozes07] consists in taming rich interactions between temporal constraints and local constraints about memory states by designing automata-based techniques in which deduction methods can be used. We follow an approach similar to [Bennett&Wolter&Zakharyaschev02] but for different spatial domains that are related to resource models such as memory states.

In the same line, we shall design separation logics including various modalities in order to deal for example with locations or temporality [Biri&Galmiche07]. The main point is to compare and share results about the specification of properties of programs with pointers.

Among the wide range of techniques that have been developed in order to achieve quantitative reasoning in various fragments of SL, little to no work has been done to investigate the theorem proving approach. The development of this approach and the design of proof-search methods will bring strong valuable contributions (more particularly w.r.t. program synthesis rather than program analysis) and complementary perspectives to quantitative reasoning in separation logics.

B) Separation and update for dynamic resources: from expressivity to decidability

After designing new resource models and identifying high-level properties that are desirable to be expressed, the next natural step consists in introducing new logical formalisms interpreted over such models and possibly to be able to express such high-level properties. The expression of (static, dynamic or high-level) properties, their combination or their abstraction are performed via adequate non-classical logics among resource logics, modal logics, temporal logics and logics with updates. This part of the project is dedicated to the introduction of new logics and to the study of their expressive power in order to justify their relevancy.

Our aims in this perspective of expressivity of the resource logics are :

To compare the resource logics between each other, in particular when considering intuitionistic versus classical operators. This amounts to define translations between resource logics that can be proved faithful semantically or by proof-theoretical means (for instance by associating corresponding proof translations).
To compare resource logics and modal logics with update semantics since both classes of logics share similarities but surprisingly, a systematic comparison has never been attempted but technical difficulties are expected.
To develop new languages for modal logics with an update semantics that can be used for reasoning about mutable data structures and their decomposition. These new languages should be sufficiently precise to express many interesting properties and support fully automatic analyses. This is a strong originality of the project.
To design symbolic representations of infinite sets of resource models to support verification and deduction tasks. The gain of expressivity is usually witnessed by the need for sophisticated symbolic representations when they exist.
To identify decidable fragments for separation logics, for instance in presence of interaction between arithmetic constraints and recursive data structures.

Designing decision procedures and proving decidability results for such logical fragments is more than just a matter of combining well-known proof-search procedures and decidability results for the underlying theories. On the contrary, one needs to understand precisely the non-trivial interaction between arithmetic constraints and recursive predicates in order to find suitable termination criteria.

C) Proof systems for separation and update logics

We aim at defining new calculi and proof systems for a wide range of resource logics. The proposal of such calculi is strongly related to the existence of resource semantics for the considered logics.

In this context the main aims and challenges are:

To design efficient algorithms that check whether a system with resources verifies a given property expressed in a logical formalism.
To define calculi and decision procedures based on proof and refutation search for extensions of separation and update logics with a strong focus on countermodel generation.
To explore approaches based on combinations of automata and proof-search techniques, depending on whether we want to check a static property (the current configuration of a network) or a dynamic property (the execution of a program with pointers).
To study the computational complexity of our algorithms in terms of time and space. In order to overcome the difficulty of dealing with resources in our systems, we shall define original symbolic representations that allow for an efficient computation of the most important operations on sets of resources.

Starting with our recently proposed calculi for BI and BBI, we shall develop and refine our original approach based on the introduction of labels and semantic constraints inside procedures that build proofs and refutations in order to combine various modalities with our central notions of separation and update.

In the context of extensions of separation and update logics as well as in the context of temporal and modal logics that include separation and spatial modalities, there is a central room for carefully designed analytic proof-search methods (with a strong focus on countermodel generation) and that such proof-methods could bring strong valuable and complementary contributions.

The thesis we defend is the following: once powerful deduction methods become available for resource logics, model-checking techniques for computer systems with resources can be enriched so as to make an efficient use of deduction steps (for instance by calling theorem-provers as subroutines at carefully chosen points of the overall model-checking process). Since such a combination of theorem-proving and model-checking approaches can only be achieved with appropriate representations of infinite sets of resource models, an originality of the project is the desire to use automata not only to encode dynamic sequences of resources but also as symbolic representations of infinite sets of resources. In addition to automata-based verification and proof-search calculi (in sequent or tableaux style), an interesting and complementary approach to characterizing provability, which has not been addressed so far in the context of resource logics, is the game-theoretic approach.

A challenging issue we would like to tackle, which indeed goes beyond the characterization of provability in resource logics, is to provide games with appropriate winning and counter-winning strategies that would provide useful hints on how to combine proof and countermodel construction and on how these two aspects could interact and exchange information during the proof-search process in order to guide it more efficiently.

Finally, we also wish to study how we can make use of tools that establish relations between various logics that are either extensions, fragments or variations of other logics. Two (non-limitative) family of tools are concerned: faithful embeddings of one logic into another one and bisimilar relations between the models of two distinct logics.