Paris, April 29th and 30th

Location: Salle 3052, Bâtiment Sophie Germain, 8 place Aurélie Nemours 75013 Paris

Monday April 29th

10h00-12h00 Discussion on future project organisation

14h00-14h45 Wrapup of the pre-scientific discussion

15h00-16h00 Stephane Demri: Modal Separation Logics and Friends

Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in order to verify programs with mutable data structures. The separating conjunction allows us to evaluate formulae in subheaps, and this possibility to evaluate formulae in alternative models is a feature shared with many modal logics such as sabotage logics, logics of public announcements or relation-changing modal logics. In the first part of the talk, we present several versions of modal separation logics whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction. Fragments are genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. In the second part of the talk, we present the decidability status and the computational complexity of several modal separation logics, (for instance, leading to NP-complete or Tower-complete satisfiability problems). In the third part, we investigate the complexity of fragments of quantified CTL under the tree semantics (or similar modal logics with propositional quantification), some of these fragments being related to modal separation logics. Part of the presented work is done jointly with B. Bednarczyk (U. of Wroclaw) or with R. Fervari (U. of Cordoba).

16h00-17h00 Alessio Mansutti: Axiomatising Logics with Separating Conjunction and Modalities

Modal separation logics are formalisms that combine modal operators to reason locally, with separating connectives that allow to perform global updates on the models. In this work, we design Hilbert-style proof systems for the modal separation logics MSL(*,<=/=>) and MSL(*,<>), where * is the separating conjunction, <> is the standard modal operator and <=/=> is the difference modality. The calculi only use the logical languages at hand (no external features such as labels) and take advantage of new normal forms and of their axiomatisation.

Tuesday April 30th

10h00-11h00 Nicolas Peltier: Towards completeness results for fragments of symbolic heaps with inductive definitions (work in progress)

In this talk, I will present some ideas and preliminary results about algorithms for testing logical entailment between symbolic heaps, in the presence of user-defined inductive predicates and interpreted theories. I will consider simple sequent-based proof procedures with explicit induction and investigate the completeness and termination of these procedures for specific fragments. We shall consider partially defined tree-like data-structures enriched with additional "local" edges and interpreted values.

11h00-12h00 Radu Iosif: Interaction Logics for Parametric Architectures

We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous atomic state changes of a set of components. We specify both the type of interactions (e.g.\ rendez-vous, broadcast) and the topology (i.e.\ architecture) of the system (e.g.\ pipeline, ring) via a decidable interaction logic, which is embedded in the classical weak sequential calculus of one successor (WS1S). Proving correctness of such system for safety properties, such as deadlock freedom or mutual exclusion, requires the inference of an inductive invariant that subsumes the set of reachable states and avoids the unsafe states. Our method synthesizes such invariants directly from the formula describing the interactions, without costly fixed point iterations. Finally, we present work in progress on the development of a separation logic of interactions, in which one specify parametric architectures using inductive definitions. Joint work with Marius Bozga and Joseph Sifakis (VERIMAG).